Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: ∃ x0 . ∃ x1 : ι → ι . MetaCat_terminal_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1.
Apply H0 with False.
Let x0 of type ι be given.
Assume H1: (λ x1 . ∃ x2 : ι → ι . MetaCat_terminal_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x1 x2) x0.
Apply H1 with False.
Let x1 of type ιι be given.
Apply H2 with False.
Apply unknownprop_2d7c7a9916fa2967cfb4d546f4e37c43b64368ed4a60618379328e066e9b7e0e with x0, λ x2 . (∀ x3 . IrreflexiveTransitiveReln x3and (BinRelnHom x3 x2 (x1 x3)) (∀ x4 . BinRelnHom x3 x2 x4x4 = x1 x3))False leaving 2 subgoals.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Let x3 of type ιιο be given.
Assume H4: ∀ x4 . x4x2not (x3 x4 x4).
Assume H5: ∀ x4 . x4x2∀ x5 . x5x2∀ x6 . x6x2x3 x4 x5x3 x5 x6x3 x4 x6.
Assume H6: ∀ x4 . IrreflexiveTransitiveReln x4and (BinRelnHom x4 (pack_r x2 x3) (x1 x4)) (∀ x5 . BinRelnHom x4 (pack_r x2 x3) x5x5 = x1 x4).
Claim L7: ...
...
Apply H6 with pack_r (prim4 x2) (λ x4 x5 . ZermeloWOstrict x4 x5), False leaving 2 subgoals.
The subproof is completed by applying L7.
Apply unknownprop_4e486761c3790f4990f398ce8c16ea7ac5915924a294f8e5b06e45030e68e983 with prim4 x2, x2, ZermeloWOstrict, x3, x1 (pack_r (prim4 x2) ZermeloWOstrict), λ x4 x5 : ο . x5(∀ x6 . BinRelnHom (pack_r (prim4 x2) ZermeloWOstrict) (pack_r x2 x3) x6x6 = x1 (pack_r (prim4 x2) ZermeloWOstrict))False.
Assume H8: and (x1 (pack_r (prim4 x2) ZermeloWOstrict)setexp x2 (prim4 x2)) (∀ x4 . x4prim4 x2∀ x5 . x5prim4 x2ZermeloWOstrict x4 x5x3 (ap (x1 (pack_r (prim4 x2) ZermeloWOstrict)) x4) (ap (x1 (pack_r (prim4 x2) ZermeloWOstrict)) x5)).
Apply H8 with (∀ x4 . BinRelnHom (pack_r (prim4 x2) ZermeloWOstrict) (pack_r x2 x3) x4x4 = x1 (pack_r (prim4 x2) ZermeloWOstrict))False.
Assume H9: x1 (pack_r (prim4 x2) (λ x4 x5 . ZermeloWOstrict x4 x5))setexp x2 (prim4 x2).
Assume H10: ∀ x4 . x4prim4 x2∀ x5 . x5prim4 x2ZermeloWOstrict x4 x5x3 (ap (x1 (pack_r (prim4 x2) (λ x6 x7 . ZermeloWOstrict x6 x7))) x4) (ap (x1 (pack_r (prim4 x2) (λ x6 x7 . ZermeloWOstrict x6 x7))) x5).
Apply FalseE with (∀ x4 . ...x4 = x1 (pack_r (prim4 x2) ...))False.
...