Metamath Proof Explorer

Theorem no2indlesm

Description: Double induction on surreals with explicit notation for the relationships. (Contributed by Scott Fenton, 22-Aug-2024)

Ref Expression
Hypotheses no2indlesm.a ⊢ R = a b | a ∈ L ⁡ b ∪ R ⁡ b
no2indlesm.1 ⊢ x = z → φ ↔ ψ
no2indlesm.2 ⊢ y = w → ψ ↔ χ
no2indlesm.3 ⊢ x = z → θ ↔ χ
no2indlesm.4 ⊢ x = A → φ ↔ τ
no2indlesm.5 ⊢ y = B → τ ↔ η
no2indlesm.i ⊢ x ∈ No ∧ y ∈ No → ∀ z ∈ L ⁡ x ∪ R ⁡ x ∀ w ∈ L ⁡ y ∪ R ⁡ y χ ∧ ∀ z ∈ L ⁡ x ∪ R ⁡ x ψ ∧ ∀ w ∈ L ⁡ y ∪ R ⁡ y θ → φ
Assertion no2indlesm ⊢ A ∈ No ∧ B ∈ No → η

Proof

Step Hyp Ref Expression
1 no2indlesm.a ⊢ R = a b | a ∈ L ⁡ b ∪ R ⁡ b
2 no2indlesm.1 ⊢ x = z → φ ↔ ψ
3 no2indlesm.2 ⊢ y = w → ψ ↔ χ
4 no2indlesm.3 ⊢ x = z → θ ↔ χ
5 no2indlesm.4 ⊢ x = A → φ ↔ τ
6 no2indlesm.5 ⊢ y = B → τ ↔ η
7 no2indlesm.i ⊢ x ∈ No ∧ y ∈ No → ∀ z ∈ L ⁡ x ∪ R ⁡ x ∀ w ∈ L ⁡ y ∪ R ⁡ y χ ∧ ∀ z ∈ L ⁡ x ∪ R ⁡ x ψ ∧ ∀ w ∈ L ⁡ y ∪ R ⁡ y θ → φ
8 1 lrrecfr ⊢ R Fr No
9 1 lrrecpo ⊢ R Po No
10 1 lrrecse ⊢ R Se No
11 1 lrrecpred ⊢ x ∈ No → Pred R No x = L ⁡ x ∪ R ⁡ x
12 11 adantr ⊢ x ∈ No ∧ y ∈ No → Pred R No x = L ⁡ x ∪ R ⁡ x
13 1 lrrecpred ⊢ y ∈ No → Pred R No y = L ⁡ y ∪ R ⁡ y
14 13 adantl ⊢ x ∈ No ∧ y ∈ No → Pred R No y = L ⁡ y ∪ R ⁡ y
15 14 raleqdv ⊢ x ∈ No ∧ y ∈ No → ∀ w ∈ Pred R No y χ ↔ ∀ w ∈ L ⁡ y ∪ R ⁡ y χ
16 12 15 raleqbidv ⊢ x ∈ No ∧ y ∈ No → ∀ z ∈ Pred R No x ∀ w ∈ Pred R No y χ ↔ ∀ z ∈ L ⁡ x ∪ R ⁡ x ∀ w ∈ L ⁡ y ∪ R ⁡ y χ
17 12 raleqdv ⊢ x ∈ No ∧ y ∈ No → ∀ z ∈ Pred R No x ψ ↔ ∀ z ∈ L ⁡ x ∪ R ⁡ x ψ
18 14 raleqdv ⊢ x ∈ No ∧ y ∈ No → ∀ w ∈ Pred R No y θ ↔ ∀ w ∈ L ⁡ y ∪ R ⁡ y θ
19 16 17 18 3anbi123d ⊢ x ∈ No ∧ y ∈ No → ∀ z ∈ Pred R No x ∀ w ∈ Pred R No y χ ∧ ∀ z ∈ Pred R No x ψ ∧ ∀ w ∈ Pred R No y θ ↔ ∀ z ∈ L ⁡ x ∪ R ⁡ x ∀ w ∈ L ⁡ y ∪ R ⁡ y χ ∧ ∀ z ∈ L ⁡ x ∪ R ⁡ x ψ ∧ ∀ w ∈ L ⁡ y ∪ R ⁡ y θ
20 19 7 sylbid ⊢ x ∈ No ∧ y ∈ No → ∀ z ∈ Pred R No x ∀ w ∈ Pred R No y χ ∧ ∀ z ∈ Pred R No x ψ ∧ ∀ w ∈ Pred R No y θ → φ
21 8 9 10 8 9 10 2 3 4 5 6 20 xpord2ind ⊢ A ∈ No ∧ B ∈ No → η