Metamath Proof Explorer

Theorem no2indslem

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

Ref Expression
Hypotheses no2indslem.a ⊢ R = a b | a ∈ L ⁡ b ∪ R ⁡ b
no2indslem.1 ⊢ x = z → φ ↔ ψ
no2indslem.2 ⊢ y = w → ψ ↔ χ
no2indslem.3 ⊢ x = z → θ ↔ χ
no2indslem.4 ⊢ x = A → φ ↔ τ
no2indslem.5 ⊢ y = B → τ ↔ η
no2indslem.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 no2indslem ⊢ A ∈ No ∧ B ∈ No → η

Proof

Step Hyp Ref Expression
1 no2indslem.a ⊢ R = a b | a ∈ L ⁡ b ∪ R ⁡ b
2 no2indslem.1 ⊢ x = z → φ ↔ ψ
3 no2indslem.2 ⊢ y = w → ψ ↔ χ
4 no2indslem.3 ⊢ x = z → θ ↔ χ
5 no2indslem.4 ⊢ x = A → φ ↔ τ
6 no2indslem.5 ⊢ y = B → τ ↔ η
7 no2indslem.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 → η