Theorem no2indslem 33740

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

Hypotheses

Ref	Expression
no2indslem.a	⊢ 𝑅 = {⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))}
no2indslem.b	⊢ 𝑆 = {⟨𝑐, 𝑑⟩ ∣ (𝑐 ∈ ( No × No ) ∧ 𝑑 ∈ ( No × No ) ∧ (((1st ‘𝑐)𝑅(1st ‘𝑑) ∨ (1st ‘𝑐) = (1st ‘𝑑)) ∧ ((2nd ‘𝑐)𝑅(2nd ‘𝑑) ∨ (2nd ‘𝑐) = (2nd ‘𝑑)) ∧ 𝑐 ≠ 𝑑))}
no2indslem.1	⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))
no2indslem.2	⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒))
no2indslem.3	⊢ (𝑥 = 𝑧 → (𝜃 ↔ 𝜒))
no2indslem.4	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
no2indslem.5	⊢ (𝑦 = 𝐵 → (𝜏 ↔ 𝜂))
no2indslem.i	⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → ((∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜒 ∧ ∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))𝜓 ∧ ∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜃) → 𝜑))

Assertion

Ref	Expression
no2indslem	⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝜂)

Distinct variable groups:   𝑎,𝑏,𝑥   𝑥,𝐴   𝑦,𝑎   𝑦,𝐴   𝑥,𝑏,𝑦   𝑦,𝐵   𝑐,𝑑   𝜒,𝑦   𝜂,𝑦   𝜑,𝑧   𝜓,𝑤,𝑥   𝑅,𝑐,𝑑   𝑤,𝑅,𝑧   𝑤,𝑆,𝑥,𝑦,𝑧   𝜏,𝑥   𝜃,𝑧   𝑥,𝑤,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑤,𝑎,𝑏,𝑐,𝑑)   𝜓(𝑦,𝑧,𝑎,𝑏,𝑐,𝑑)   𝜒(𝑥,𝑧,𝑤,𝑎,𝑏,𝑐,𝑑)   𝜃(𝑥,𝑦,𝑤,𝑎,𝑏,𝑐,𝑑)   𝜏(𝑦,𝑧,𝑤,𝑎,𝑏,𝑐,𝑑)   𝜂(𝑥,𝑧,𝑤,𝑎,𝑏,𝑐,𝑑)   𝐴(𝑧,𝑤,𝑎,𝑏,𝑐,𝑑)   𝐵(𝑥,𝑧,𝑤,𝑎,𝑏,𝑐,𝑑)   𝑅(𝑥,𝑦,𝑎,𝑏)   𝑆(𝑎,𝑏,𝑐,𝑑)

Proof of Theorem no2indslem

Step	Hyp	Ref	Expression
1		no2indslem.b	. 2 ⊢ 𝑆 = {⟨𝑐, 𝑑⟩ ∣ (𝑐 ∈ ( No × No ) ∧ 𝑑 ∈ ( No × No ) ∧ (((1st ‘𝑐)𝑅(1st ‘𝑑) ∨ (1st ‘𝑐) = (1st ‘𝑑)) ∧ ((2nd ‘𝑐)𝑅(2nd ‘𝑑) ∨ (2nd ‘𝑐) = (2nd ‘𝑑)) ∧ 𝑐 ≠ 𝑑))}
2		no2indslem.a	. . 3 ⊢ 𝑅 = {⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))}
3	2	lrrecfr 33729	. 2 ⊢ 𝑅 Fr No
4	2	lrrecpo 33727	. 2 ⊢ 𝑅 Po No
5	2	lrrecse 33728	. 2 ⊢ 𝑅 Se No
6		no2indslem.1	. 2 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))
7		no2indslem.2	. 2 ⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒))
8		no2indslem.3	. 2 ⊢ (𝑥 = 𝑧 → (𝜃 ↔ 𝜒))
9		no2indslem.4	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
10		no2indslem.5	. 2 ⊢ (𝑦 = 𝐵 → (𝜏 ↔ 𝜂))
11	2	lrrecpred 33730	. . . . . 6 ⊢ (𝑥 ∈ No → Pred(𝑅, No , 𝑥) = (( L ‘𝑥) ∪ ( R ‘𝑥)))
12	11	adantr 484	. . . . 5 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → Pred(𝑅, No , 𝑥) = (( L ‘𝑥) ∪ ( R ‘𝑥)))
13	2	lrrecpred 33730	. . . . . . 7 ⊢ (𝑦 ∈ No → Pred(𝑅, No , 𝑦) = (( L ‘𝑦) ∪ ( R ‘𝑦)))
14	13	adantl 485	. . . . . 6 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → Pred(𝑅, No , 𝑦) = (( L ‘𝑦) ∪ ( R ‘𝑦)))
15	14	raleqdv 3315	. . . . 5 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → (∀𝑤 ∈ Pred (𝑅, No , 𝑦)𝜒 ↔ ∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜒))
16	12, 15	raleqbidv 3303	. . . 4 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → (∀𝑧 ∈ Pred (𝑅, No , 𝑥)∀𝑤 ∈ Pred (𝑅, No , 𝑦)𝜒 ↔ ∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜒))
17	12	raleqdv 3315	. . . 4 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → (∀𝑧 ∈ Pred (𝑅, No , 𝑥)𝜓 ↔ ∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))𝜓))
18	14	raleqdv 3315	. . . 4 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → (∀𝑤 ∈ Pred (𝑅, No , 𝑦)𝜃 ↔ ∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜃))
19	16, 17, 18	3anbi123d 1437	. . 3 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → ((∀𝑧 ∈ Pred (𝑅, No , 𝑥)∀𝑤 ∈ Pred (𝑅, No , 𝑦)𝜒 ∧ ∀𝑧 ∈ Pred (𝑅, No , 𝑥)𝜓 ∧ ∀𝑤 ∈ Pred (𝑅, No , 𝑦)𝜃) ↔ (∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜒 ∧ ∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))𝜓 ∧ ∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜃)))
20		no2indslem.i	. . 3 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → ((∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜒 ∧ ∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))𝜓 ∧ ∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜃) → 𝜑))
21	19, 20	sylbid 243	. 2 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → ((∀𝑧 ∈ Pred (𝑅, No , 𝑥)∀𝑤 ∈ Pred (𝑅, No , 𝑦)𝜒 ∧ ∀𝑧 ∈ Pred (𝑅, No , 𝑥)𝜓 ∧ ∀𝑤 ∈ Pred (𝑅, No , 𝑦)𝜃) → 𝜑))
22	1, 3, 4, 5, 3, 4, 5, 6, 7, 8, 9, 10, 21	xpord2ind 33397	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝜂)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2113   ≠ wne 2934  ∀wral 3053   ∪ cun 3839   class class class wbr 5027  {copab 5089   × cxp 5517  Predcpred 6122  ‘cfv 6333  1^st c1st 7705  2^nd c2nd 7706   No csur 33476   L cleft 33662   R cright 33663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-int 4834  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6123  df-ord 6169  df-on 6170  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7121  df-ov 7167  df-oprab 7168  df-mpo 7169  df-1st 7707  df-2nd 7708  df-wrecs 7969  df-recs 8030  df-1o 8124  df-2o 8125  df-no 33479  df-slt 33480  df-bday 33481  df-sslt 33609  df-scut 33611  df-made 33664  df-old 33665  df-left 33667  df-right 33668

This theorem is referenced by:  no2inds  33741