Metamath Proof Explorer

Theorem on2ind

Description: Double induction over ordinal numbers. (Contributed by Scott Fenton, 26-Aug-2024)

Ref Expression
Hypotheses on2ind.1 ⊢ a = c → φ ↔ ψ
on2ind.2 ⊢ b = d → ψ ↔ χ
on2ind.3 ⊢ a = c → θ ↔ χ
on2ind.4 ⊢ a = X → φ ↔ τ
on2ind.5 ⊢ b = Y → τ ↔ η
on2ind.i ⊢ a ∈ On ∧ b ∈ On → ∀ c ∈ a ∀ d ∈ b χ ∧ ∀ c ∈ a ψ ∧ ∀ d ∈ b θ → φ
Assertion on2ind ⊢ X ∈ On ∧ Y ∈ On → η

Proof

Step Hyp Ref Expression
1 on2ind.1 ⊢ a = c → φ ↔ ψ
2 on2ind.2 ⊢ b = d → ψ ↔ χ
3 on2ind.3 ⊢ a = c → θ ↔ χ
4 on2ind.4 ⊢ a = X → φ ↔ τ
5 on2ind.5 ⊢ b = Y → τ ↔ η
6 on2ind.i ⊢ a ∈ On ∧ b ∈ On → ∀ c ∈ a ∀ d ∈ b χ ∧ ∀ c ∈ a ψ ∧ ∀ d ∈ b θ → φ
7 eqid ⊢ x y | x ∈ On × On ∧ y ∈ On × On ∧ 1 st ⁡ x E 1 st ⁡ y ∨ 1 st ⁡ x = 1 st ⁡ y ∧ 2 nd ⁡ x E 2 nd ⁡ y ∨ 2 nd ⁡ x = 2 nd ⁡ y ∧ x ≠ y = x y | x ∈ On × On ∧ y ∈ On × On ∧ 1 st ⁡ x E 1 st ⁡ y ∨ 1 st ⁡ x = 1 st ⁡ y ∧ 2 nd ⁡ x E 2 nd ⁡ y ∨ 2 nd ⁡ x = 2 nd ⁡ y ∧ x ≠ y
8 onfr ⊢ E Fr On
9 epweon ⊢ E We On
10 weso ⊢ E We On → E Or On
11 sopo ⊢ E Or On → E Po On
12 9 10 11 mp2b ⊢ E Po On
13 epse ⊢ E Se On
14 predon ⊢ a ∈ On → Pred E On a = a
15 14 adantr ⊢ a ∈ On ∧ b ∈ On → Pred E On a = a
16 predon ⊢ b ∈ On → Pred E On b = b
17 16 adantl ⊢ a ∈ On ∧ b ∈ On → Pred E On b = b
18 17 raleqdv ⊢ a ∈ On ∧ b ∈ On → ∀ d ∈ Pred E On b χ ↔ ∀ d ∈ b χ
19 15 18 raleqbidv ⊢ a ∈ On ∧ b ∈ On → ∀ c ∈ Pred E On a ∀ d ∈ Pred E On b χ ↔ ∀ c ∈ a ∀ d ∈ b χ
20 15 raleqdv ⊢ a ∈ On ∧ b ∈ On → ∀ c ∈ Pred E On a ψ ↔ ∀ c ∈ a ψ
21 17 raleqdv ⊢ a ∈ On ∧ b ∈ On → ∀ d ∈ Pred E On b θ ↔ ∀ d ∈ b θ
22 19 20 21 3anbi123d ⊢ a ∈ On ∧ b ∈ On → ∀ c ∈ Pred E On a ∀ d ∈ Pred E On b χ ∧ ∀ c ∈ Pred E On a ψ ∧ ∀ d ∈ Pred E On b θ ↔ ∀ c ∈ a ∀ d ∈ b χ ∧ ∀ c ∈ a ψ ∧ ∀ d ∈ b θ
23 22 6 sylbid ⊢ a ∈ On ∧ b ∈ On → ∀ c ∈ Pred E On a ∀ d ∈ Pred E On b χ ∧ ∀ c ∈ Pred E On a ψ ∧ ∀ d ∈ Pred E On b θ → φ
24 7 8 12 13 8 12 13 1 2 3 4 5 23 xpord2ind ⊢ X ∈ On ∧ Y ∈ On → η