Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ∀ x0 . nat_p x0 ⟶ Inj1 x0 = ordsucc x0
Apply nat_complete_ind with λ x0 . Inj1 x0 = ordsucc x0.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: ∀ x1 . x1 ∈ x0 ⟶ Inj1 x1 = ordsucc x1.
Apply set_ext with Inj1 x0, ordsucc x0 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H2: x1 ∈ Inj1 x0.
Apply Inj1E with x0, x1, x1 ∈ ordsucc x0 leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H3: x1 = 0.
Apply H3 with λ x2 x3 . x3 ∈ ordsucc x0.
Apply nat_0_in_ordsucc with x0.
The subproof is completed by applying H0.
Assume H3: ∃ x2 . and (x2 ∈ x0) (x1 = Inj1 x2).
Apply exandE_i with λ x2 . x2 ∈ x0, λ x2 . x1 = Inj1 x2, x1 ∈ ordsucc x0 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Assume H4: x2 ∈ x0.
Assume H5: x1 = Inj1 x2.
Apply H5 with λ x3 x4 . x4 ∈ ordsucc x0.
Apply H1 with x2, λ x3 x4 . x4 ∈ ordsucc x0 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply nat_ordsucc_in_ordsucc with x0, x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Let x1 of type ι be given.
Assume H2: x1 ∈ ordsucc x0.
Apply ordsuccE with x0, x1, x1 ∈ Inj1 x0 leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H3: x1 ∈ x0.
Apply nat_inv with x1, x1 ∈ Inj1 x0 leaving 3 subgoals.
Apply nat_p_trans with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Assume H4: x1 = 0.
Apply H4 with λ x2 x3 . x3 ∈ Inj1 x0.
The subproof is completed by applying Inj1I1 with x0.
Assume H4: ∃ x2 . and (nat_p x2) (x1 = ordsucc x2).
Apply exandE_i with nat_p, λ x2 . x1 = ordsucc x2, x1 ∈ Inj1 x0 leaving 2 subgoals.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Assume H5: nat_p x2.
Assume H6: x1 = ordsucc x2.
Apply H6 with λ x3 x4 . x4 ∈ Inj1 x0.
Claim L7: x2 ∈ x1
Apply H6 with λ x3 x4 . x2 ∈ x4.
The subproof is completed by applying ordsuccI2 with x2.
Claim L8: x2 ∈ x0
Apply nat_trans with x0, x1, x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying L7.
Apply H1 with x2, λ x3 x4 . x3 ∈ Inj1 x0 leaving 2 subgoals.
The subproof is completed by applying L8.
Apply Inj1I2 with x0, x2.
The subproof is completed by applying L8.
Assume H3: x1 = x0.
Apply H3 with λ x2 x3 . x3 ∈ Inj1 x0.
Apply nat_inv with x0, x0 ∈ Inj1 x0 leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H4: x0 = 0.
Apply H4 with λ x2 x3 . x3 ∈ Inj1 x0.
The subproof is completed by applying Inj1I1 with x0.
Assume H4: ∃ x2 . and (nat_p x2) (x0 = ordsucc x2).
Apply exandE_i with nat_p, λ x2 . x0 = ordsucc x2, x0 ∈ Inj1 x0 leaving 2 subgoals.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Assume H5: nat_p x2.
Assume H6: x0 = ordsucc x2.
Apply H6 with λ x3 x4 . x4 ∈ Inj1 x0.
Claim L7: x2 ∈ x0
Apply H6 with λ x3 x4 . x2 ∈ x4.
The subproof is completed by applying ordsuccI2 with x2.
Apply H1 with x2, λ x3 x4 . x3 ∈ Inj1 x0 leaving 2 subgoals.
The subproof is completed by applying L7.
Apply Inj1I2 with x0, x2.
The subproof is completed by applying L7.
Let x0 of type ι be given.
Assume H1: nat_p x0.
Apply Inj1_setsum_1L with x0, λ x1 x2 . x2 = ordsucc x0.
Apply L0 with x0.
The subproof is completed by applying H1.
■