Let x0 of type ι be given.
Let x1 of type ι be given.
Apply xm with
x0 = x1,
finite (UPair x0 x1) leaving 2 subgoals.
Assume H0: x0 = x1.
Apply H0 with
λ x2 x3 . finite (UPair x0 x2).
Apply set_ext with
UPair x0 x0,
Sing x0 leaving 2 subgoals.
Let x2 of type ι be given.
Assume H1:
x2 ∈ UPair x0 x0.
Apply UPairE with
x2,
x0,
x0,
x2 ∈ Sing x0 leaving 3 subgoals.
The subproof is completed by applying H1.
Assume H2: x2 = x0.
Apply H2 with
λ x3 x4 . x4 ∈ Sing x0.
The subproof is completed by applying SingI with x0.
Assume H2: x2 = x0.
Apply H2 with
λ x3 x4 . x4 ∈ Sing x0.
The subproof is completed by applying SingI with x0.
Apply unknownprop_158329ee42f538f9f45353e081644457b58bf58b995713ab00dcbc514147ba46 with
UPair x0 x0,
x0.
The subproof is completed by applying UPairI1 with x0, x0.
Apply L1 with
λ x2 x3 . finite x3.
The subproof is completed by applying unknownprop_f7016afae9c8976834aae8fd87dfbc66905d8d8b02412954fb76543365d9f363 with x0.
Assume H0: x0 = x1 ⟶ ∀ x2 : ο . x2.
Let x2 of type ο be given.
Apply H1 with
u2.
Apply andI with
u2 ∈ omega,
equip (UPair x0 x1) u2 leaving 2 subgoals.
Apply nat_p_omega with
u2.
The subproof is completed by applying nat_2.
Apply unknownprop_39df499f773ced696ac600b0767cd28b9ceea72e50ff2c9103bc16896281c585 with
x0,
x1.
The subproof is completed by applying H0.