Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 80242.. x0.
Claim L1: ordinal (e4431.. x0)
...
Claim L2: ∀ x1 . prim1 x1 (23e07.. x0) ⟶ 80242.. x1
Let x1 of type ι be given.
Assume H2: prim1 x1 (23e07.. x0).
Claim L3: prim1 x1 (56ded.. (e4431.. x0))
Apply unknownprop_78dd4d18930f8cdb1d353eca6deb6db797599b58a01b747c9a28b7030299025c with 56ded.. (e4431.. x0), λ x2 . 099f3.. x2 x0, x1.
The subproof is completed by applying H2.
Apply unknownprop_08307bdbb7a97185122351ee4a5953158d8e3481a107df1f643fe83793e0fbe1 with e4431.. x0, x1, ∃ x2 . and (ordinal x2) (1beb9.. x2 x1) leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L3.
Let x2 of type ι be given.
Assume H4: (λ x3 . and (prim1 x3 (e4431.. x0)) (1beb9.. x3 x1)) x2.
Apply H4 with ∃ x3 . and (ordinal x3) (1beb9.. x3 x1).
Assume H5: prim1 x2 (e4431.. x0).
Assume H6: 1beb9.. x2 x1.
Let x3 of type ο be given.
Assume H7: ∀ x4 . and (ordinal x4) (1beb9.. x4 x1) ⟶ x3.
Apply H7 with x2.
Apply andI with ordinal x2, 1beb9.. x2 x1 leaving 2 subgoals.
Apply ordinal_Hered with e4431.. x0, x2 leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Claim L3: ∀ x1 . prim1 x1 (5246e.. x0) ⟶ 80242.. x1
Let x1 of type ι be given.
Assume H3: prim1 x1 (5246e.. x0).
Claim L4: prim1 x1 (56ded.. (e4431.. x0))
Apply unknownprop_78dd4d18930f8cdb1d353eca6deb6db797599b58a01b747c9a28b7030299025c with 56ded.. (e4431.. x0), λ x2 . 099f3.. x0 x2, x1.
The subproof is completed by applying H3.
Apply unknownprop_08307bdbb7a97185122351ee4a5953158d8e3481a107df1f643fe83793e0fbe1 with e4431.. x0, x1, ∃ x2 . and (ordinal x2) (1beb9.. x2 x1) leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L4.
Let x2 of type ι be given.
Assume H5: (λ x3 . and (prim1 x3 (e4431.. x0)) (1beb9.. x3 x1)) x2.
Apply H5 with ∃ x3 . and (ordinal x3) (1beb9.. x3 x1).
Assume H6: prim1 x2 (e4431.. x0).
Assume H7: 1beb9.. x2 x1.
Let x3 of type ο be given.
Assume H8: ∀ x4 . and (ordinal x4) (1beb9.. x4 x1) ⟶ x3.
Apply H8 with x2.
Apply andI with ordinal x2, 1beb9.. x2 x1 leaving 2 subgoals.
Apply ordinal_Hered with e4431.. x0, x2 leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
Claim L4: ∀ x1 . prim1 x1 (23e07.. x0) ⟶ ∀ x2 . prim1 x2 (5246e.. x0) ⟶ 099f3.. x1 x2
Let x1 of type ι be given.
Assume H4: prim1 x1 (23e07.. x0).
Let x2 of type ι be given.
Assume H5: prim1 x2 (5246e.. x0).
Apply unknownprop_fb545b225a42993d98e0d062b6c9208b8321e87814f4e26de3418c134068c2c8 with x1, x0, x2 leaving 5 subgoals.
Apply L2 with x1.
The subproof is completed by applying H4.
The subproof is completed by applying H0.
Apply L3 with x2.
The subproof is completed by applying H5.
Apply unknownprop_e75b5686f39ea4dca8e72e616b0514162494e9e895f52dbe14fa1984a713fe57 with 56ded.. (e4431.. x0), λ x3 . 099f3.. x3 x0, x1.
The subproof is completed by applying H4.
Apply unknownprop_e75b5686f39ea4dca8e72e616b0514162494e9e895f52dbe14fa1984a713fe57 with 56ded.. (e4431.. x0), λ x3 . 099f3.. x0 x3, x2.
The subproof is completed by applying H5.
Apply and3I with ∀ x1 . prim1 x1 (23e07.. x0) ⟶ 80242.. x1, ∀ x1 . prim1 x1 (5246e.. x0) ⟶ 80242.. x1, ∀ x1 . prim1 x1 (23e07.. x0) ⟶ ∀ x2 . prim1 x2 (5246e.. x0) ⟶ 099f3.. x1 x2 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
■