Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: equip x0 u3.
Apply equip_tra with {x1 ∈ prim4 x0|equip x1 u2}, {x1 ∈ prim4 u3|equip x1 u2}, u3 leaving 2 subgoals.
Apply H0 with equip {x1 ∈ prim4 x0|equip x1 u2} {x1 ∈ prim4 u3|equip x1 u2}.
Let x1 of type ιι be given.
Assume H1: bij x0 u3 x1.
Apply bijE with x0, u3, x1, equip {x2 ∈ prim4 x0|equip x2 u2} {x2 ∈ prim4 u3|equip x2 u2} leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2: ∀ x2 . x2x0x1 x2u3.
Assume H3: ∀ x2 . x2x0∀ x3 . x3x0x1 x2 = x1 x3x2 = x3.
Assume H4: ∀ x2 . x2u3∃ x3 . and (x3x0) (x1 x3 = x2).
Claim L5: ...
...
Apply bijE with u3, x0, inv x0 x1, equip {x2 ∈ prim4 x0|equip x2 u2} {x2 ∈ prim4 u3|equip x2 u2} leaving 2 subgoals.
The subproof is completed by applying L5.
Assume H6: ∀ x2 . x2u3inv x0 x1 x2x0.
Assume H7: ∀ x2 . x2u3∀ x3 . x3u3inv x0 x1 x2 = inv x0 x1 x3x2 = x3.
Assume H8: ∀ x2 . x2x0∃ x3 . and (x3u3) (inv x0 x1 x3 = x2).
Let x2 of type ο be given.
Assume H9: ∀ x3 : ι → ι . bij {x4 ∈ prim4 x0|equip x4 u2} {x4 ∈ prim4 u3|equip x4 u2} x3x2.
Apply H9 with λ x3 . {x1 x4|x4 ∈ x3}.
Apply bijI with {x3 ∈ prim4 x0|equip x3 u2}, {x3 ∈ prim4 u3|equip x3 u2}, λ x3 . {x1 x4|x4 ∈ x3} leaving 3 subgoals.
Let x3 of type ι be given.
Assume H10: x3{x4 ∈ prim4 x0|equip x4 u2}.
Apply SepE with prim4 x0, λ x4 . equip x4 u2, x3, (λ x4 . {x1 x5|x5 ∈ x4}) x3{x4 ∈ prim4 u3|equip x4 u2} leaving 2 subgoals.
The subproof is completed by applying H10.
Assume H11: x3prim4 x0.
Assume H12: equip x3 u2.
Apply SepI with prim4 u3, λ x4 . equip x4 u2, (λ x4 . {x1 x5|x5 ∈ x4}) x3 leaving 2 subgoals.
Apply PowerI with u3, {x1 x4|x4 ∈ x3}.
Let x4 of type ι be given.
Assume H13: x4{x1 x5|x5 ∈ x3}.
Apply ReplE_impred with x3, x1, x4, x4u3 leaving 2 subgoals.
The subproof is completed by applying H13.
Let x5 of type ι be given.
Assume H14: x5x3.
Assume H15: x4 = x1 x5.
Apply H15 with λ x6 x7 . x7u3.
Apply H2 with x5.
Apply PowerE with x0, x3, x5 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying H14.
Apply equip_tra with {...|x4 ∈ x3}, ..., ... leaving 2 subgoals.
...
...
...
...
...