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 onfr ⊢ E Fr On
8 epweon ⊢ E We On
9 weso ⊢ E We On → E Or On
10 sopo ⊢ E Or On → E Po On
11 8 9 10 mp2b ⊢ E Po On
12 epse ⊢ E Se On
13 predon ⊢ a ∈ On → Pred E On a = a
14 13 adantr ⊢ a ∈ On ∧ b ∈ On → Pred E On a = a
15 predon ⊢ b ∈ On → Pred E On b = b
16 15 adantl ⊢ a ∈ On ∧ b ∈ On → Pred E On b = b
17 16 raleqdv ⊢ a ∈ On ∧ b ∈ On → ∀ d ∈ Pred E On b χ ↔ ∀ d ∈ b χ
18 14 17 raleqbidv ⊢ a ∈ On ∧ b ∈ On → ∀ c ∈ Pred E On a ∀ d ∈ Pred E On b χ ↔ ∀ c ∈ a ∀ d ∈ b χ
19 14 raleqdv ⊢ a ∈ On ∧ b ∈ On → ∀ c ∈ Pred E On a ψ ↔ ∀ c ∈ a ψ
20 16 raleqdv ⊢ a ∈ On ∧ b ∈ On → ∀ d ∈ Pred E On b θ ↔ ∀ d ∈ b θ
21 18 19 20 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 θ
22 21 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 θ → φ
23 7 11 12 7 11 12 1 2 3 4 5 22 xpord2ind ⊢ X ∈ On ∧ Y ∈ On → η