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: equip x0 x1.
Assume H1: equip x2 x3.
Apply H0 with equip (setprod x0 x2) (setprod x1 x3).
Let x4 of type ιι be given.
Assume H2: bij x0 x1 x4.
Apply bijE with x0, x1, x4, equip (setprod x0 x2) (setprod x1 x3) leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H3: ∀ x5 . x5x0x4 x5x1.
Assume H4: ∀ x5 . x5x0∀ x6 . x6x0x4 x5 = x4 x6x5 = x6.
Assume H5: ∀ x5 . x5x1∃ x6 . and (x6x0) (x4 x6 = x5).
Apply H1 with equip (setprod x0 x2) (setprod x1 x3).
Let x5 of type ιι be given.
Assume H6: bij x2 x3 x5.
Apply bijE with x2, x3, x5, equip (setprod x0 x2) (setprod x1 x3) leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H7: ∀ x6 . x6x2x5 x6x3.
Assume H8: ∀ x6 . x6x2∀ x7 . x7x2x5 x6 = x5 x7x6 = x7.
Assume H9: ∀ x6 . x6x3∃ x7 . and (x7x2) (x5 x7 = x6).
Let x6 of type ο be given.
Assume H10: ∀ x7 : ι → ι . bij (setprod x0 x2) (setprod x1 x3) x7x6.
Apply H10 with λ x7 . lam 2 (λ x8 . If_i (x8 = 0) (x4 (ap x7 0)) (x5 (ap x7 1))).
Apply bijI with setprod x0 x2, setprod x1 x3, λ x7 . lam 2 (λ x8 . If_i (x8 = 0) (x4 (ap x7 0)) (x5 (ap x7 1))) leaving 3 subgoals.
Let x7 of type ι be given.
Assume H11: x7setprod x0 x2.
Apply tuple_2_setprod with x1, x3, x4 (ap x7 0), x5 (ap x7 1) leaving 2 subgoals.
Apply H3 with ap x7 0.
Apply ap0_Sigma with x0, λ x8 . x2, x7.
The subproof is completed by applying H11.
Apply H7 with ap x7 1.
Apply ap1_Sigma with x0, λ x8 . x2, x7.
The subproof is completed by applying H11.
Let x7 of type ι be given.
Assume H11: x7setprod x0 x2.
Let x8 of type ι be given.
Assume H12: x8setprod x0 x2.
Assume H13: lam 2 (λ x9 . If_i (x9 = 0) (x4 (ap x7 0)) (x5 (ap x7 1))) = lam 2 (λ x9 . If_i (x9 = 0) (x4 (ap x8 0)) (x5 (ap x8 1))).
Apply tuple_Sigma_eta with x0, λ x9 . x2, x7, λ x9 x10 . x9 = x8 leaving 2 subgoals.
The subproof is completed by applying H11.
Apply tuple_Sigma_eta with x0, λ x9 . x2, x8, λ x9 x10 . lam 2 (λ x11 . If_i (x11 = 0) ... ...) = ... leaving 2 subgoals.
...
...
...