Let x0 of type ο be given.
Claim L0:
(λ x1 . or (x1 = 0) x0) 0Apply orIL with
0 = 0,
x0.
Let x1 of type ι → ι → ο be given.
Assume H0: x1 0 0.
The subproof is completed by applying H0.
Claim L1:
or (prim0 (λ x1 . or (x1 = 0) x0) = 0) x0Apply Eps_i_ax with
λ x1 . or (x1 = 0) x0,
0.
The subproof is completed by applying L0.
Claim L2:
(λ x1 . or (x1 = 0 ⟶ ∀ x2 : ο . x2) x0) (prim4 0)Apply orIL with
not (prim4 0 = 0),
x0.
Apply EmptyE with
0.
Apply H2 with
λ x1 x2 . 0 ∈ x1.
The subproof is completed by applying Empty_In_Power with 0.
Claim L3:
or (prim0 (λ x1 . or (x1 = 0 ⟶ ∀ x2 : ο . x2) x0) = 0 ⟶ ∀ x1 : ο . x1) x0Apply Eps_i_ax with
λ x1 . or (x1 = 0 ⟶ ∀ x2 : ο . x2) x0,
prim4 0.
The subproof is completed by applying L2.
Apply L1 with
or x0 (not x0) leaving 2 subgoals.
Assume H4:
prim0 (λ x1 . or (x1 = 0) x0) = 0.
Apply L3 with
or x0 (not x0) leaving 2 subgoals.
Assume H5:
prim0 (λ x1 . or (x1 = 0 ⟶ ∀ x2 : ο . x2) x0) = 0 ⟶ ∀ x1 : ο . x1.
Apply orIR with
x0,
not x0.
Assume H6: x0.
Claim L7:
(λ x1 . or (x1 = 0) x0) = λ x1 . or (x1 = 0 ⟶ ∀ x2 : ο . x2) x0Apply pred_ext with
λ x1 . or (x1 = 0) x0,
λ x1 . or (x1 = 0 ⟶ ∀ x2 : ο . x2) x0.
Let x1 of type ι be given.
Apply iffI with
(λ x2 . or (x2 = 0) x0) x1,
(λ x2 . or (x2 = 0 ⟶ ∀ x3 : ο . x3) x0) x1 leaving 2 subgoals.
Assume H7:
(λ x2 . or (x2 = 0) x0) x1.
Apply orIR with
not (x1 = 0),
x0.
The subproof is completed by applying H6.
Assume H7:
(λ x2 . or (x2 = 0 ⟶ ∀ x3 : ο . x3) x0) x1.
Apply orIR with
x1 = 0,
x0.
The subproof is completed by applying H6.
Apply H5.
Apply L7 with
λ x1 x2 : ι → ο . prim0 x1 = 0.
The subproof is completed by applying H4.
Assume H5: x0.
Apply orIL with
x0,
not x0.
The subproof is completed by applying H5.
Assume H4: x0.
Apply orIL with
x0,
not x0.
The subproof is completed by applying H4.