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.b ⊢ S = c d | c ∈ No × No ∧ d ∈ No × No ∧ 1 st ⁡ c R 1 st ⁡ d ∨ 1 st ⁡ c = 1 st ⁡ d ∧ 2 nd ⁡ c R 2 nd ⁡ d ∨ 2 nd ⁡ c = 2 nd ⁡ d ∧ c ≠ d
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.b ⊢ S = c d | c ∈ No × No ∧ d ∈ No × No ∧ 1 st ⁡ c R 1 st ⁡ d ∨ 1 st ⁡ c = 1 st ⁡ d ∧ 2 nd ⁡ c R 2 nd ⁡ d ∨ 2 nd ⁡ c = 2 nd ⁡ d ∧ c ≠ d
3 no2indslem.1 ⊢ x = z → φ ↔ ψ
4 no2indslem.2 ⊢ y = w → ψ ↔ χ
5 no2indslem.3 ⊢ x = z → θ ↔ χ
6 no2indslem.4 ⊢ x = A → φ ↔ τ
7 no2indslem.5 ⊢ y = B → τ ↔ η
8 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 θ → φ
9 1 lrrecfr ⊢ R Fr No
10 1 lrrecpo ⊢ R Po No
11 1 lrrecse ⊢ R Se No
12 1 lrrecpred ⊢ x ∈ No → Pred R No x = L ⁡ x ∪ R ⁡ x
13 12 adantr ⊢ x ∈ No ∧ y ∈ No → Pred R No x = L ⁡ x ∪ R ⁡ x
14 1 lrrecpred ⊢ y ∈ No → Pred R No y = L ⁡ y ∪ R ⁡ y
15 14 adantl ⊢ x ∈ No ∧ y ∈ No → Pred R No y = L ⁡ y ∪ R ⁡ y
16 15 raleqdv ⊢ x ∈ No ∧ y ∈ No → ∀ w ∈ Pred R No y χ ↔ ∀ w ∈ L ⁡ y ∪ R ⁡ y χ
17 13 16 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 χ
18 13 raleqdv ⊢ x ∈ No ∧ y ∈ No → ∀ z ∈ Pred R No x ψ ↔ ∀ z ∈ L ⁡ x ∪ R ⁡ x ψ
19 15 raleqdv ⊢ x ∈ No ∧ y ∈ No → ∀ w ∈ Pred R No y θ ↔ ∀ w ∈ L ⁡ y ∪ R ⁡ y θ
20 17 18 19 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 θ
21 20 8 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 θ → φ
22 2 9 10 11 9 10 11 3 4 5 6 7 21 xpord2ind ⊢ A ∈ No ∧ B ∈ No → η