Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ιι be given.
Let x3 of type ιι be given.
Assume H0: inj x0 x1 x2.
Assume H1: inj x1 x0 x3.
Apply H0 with equip x0 x1.
Assume H2: ∀ x4 . x4x0x2 x4x1.
Assume H3: ∀ x4 . x4x0∀ x5 . x5x0x2 x4 = x2 x5x4 = x5.
Apply H1 with equip x0 x1.
Assume H4: ∀ x4 . x4x1x3 x4x0.
Assume H5: ∀ x4 . x4x1∀ x5 . x5x1x3 x4 = x3 x5x4 = x5.
Claim L6: ...
...
Claim L7: ...
...
Apply KnasterTarski_set with x0, λ x4 . {x3 x5|x5 ∈ setminus x1 {x2 x5|x5 ∈ setminus x0 x4}}, equip x0 x1 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
Let x4 of type ι be given.
Assume H8: (λ x5 . and (x5prim4 x0) (prim5 (setminus x1 (prim5 (setminus x0 x5) x2)) x3 = x5)) x4.
Apply H8 with equip x0 x1.
Assume H9: x4prim4 x0.
Assume H10: (λ x5 . {x3 x6|x6 ∈ setminus x1 {x2 x6|x6 ∈ setminus x0 x5}}) x4 = x4.
Let x5 of type ο be given.
Assume H11: ∀ x6 : ι → ι . bij x0 x1 x6x5.
Apply H11 with λ x6 . If_i (x6x4) (inv x1 x3 x6) (x2 x6).
Apply bijI with x0, x1, λ x6 . If_i (x6x4) (inv x1 x3 x6) (x2 x6) leaving 3 subgoals.
Let x6 of type ι be given.
Assume H12: x6x0.
Apply xm with x6x4, If_i (x6x4) (inv x1 x3 x6) (x2 x6)x1 leaving 2 subgoals.
Assume H13: x6x4.
Apply If_i_1 with x6x4, inv x1 x3 x6, x2 x6, λ x7 x8 . x8x1 leaving 2 subgoals.
The subproof is completed by applying H13.
Claim L14: x6(λ x7 . {x3 x8|x8 ∈ setminus x1 {x2 x8|x8 ∈ setminus x0 x7}}) x4
Apply H10 with λ x7 x8 . x6x8.
The subproof is completed by applying H13.
Apply ReplE_impred with setminus x1 {x2 x7|x7 ∈ setminus x0 x4}, x3, x6, inv x1 x3 x6x1 leaving 2 subgoals.
The subproof is completed by applying L14.
Let x7 of type ι be given.
Assume H15: x7setminus x1 {x2 x8|x8 ∈ setminus x0 x4}.
Assume H16: x6 = x3 x7.
Claim L17: x7x1
Apply setminusE1 with x1, {x2 x8|x8 ∈ setminus x0 x4}, x7.
The subproof is completed by applying H15.
Apply H16 with λ x8 x9 . inv x1 x3 x9x1.
Apply inj_linv_coddep with x1, x0, x3, x7, λ x8 x9 . x9x1 leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying L17.
The subproof is completed by applying L17.
Assume H13: nIn x6 x4.
...
...
...