Theorem no3inds 33699

Description: Triple induction over surreal numbers. The substitution instances cover all possible instances of less than or equal to x, y, and z. (Contributed by Scott Fenton, 21-Aug-2024.)

Hypotheses

Ref	Expression
no3inds.1	⊢ (𝑝 = 𝑞 → (𝜑 ↔ 𝜓))
no3inds.2	⊢ (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝜑 ↔ 𝜒))
no3inds.3	⊢ (𝑞 = ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ → (𝜓 ↔ 𝜃))
no3inds.4	⊢ (𝑢 = 𝑧 → (𝜃 ↔ 𝜏))
no3inds.5	⊢ (𝑡 = 𝑦 → (𝜃 ↔ 𝜂))
no3inds.6	⊢ (𝑢 = 𝑧 → (𝜂 ↔ 𝜁))
no3inds.7	⊢ (𝑤 = 𝑥 → (𝜃 ↔ 𝜎))
no3inds.8	⊢ (𝑢 = 𝑧 → (𝜎 ↔ 𝜌))
no3inds.9	⊢ (𝑡 = 𝑦 → (𝜎 ↔ 𝜇))
no3inds.10	⊢ (𝑥 = 𝐴 → (𝜒 ↔ 𝜆))
no3inds.11	⊢ (𝑦 = 𝐵 → (𝜆 ↔ 𝜅))
no3inds.12	⊢ (𝑧 = 𝐶 → (𝜅 ↔ 𝛻))
no3inds.i	⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → (((∀𝑤 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑡 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑢 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))𝜃 ∧ ∀𝑤 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑡 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜏 ∧ ∀𝑤 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑢 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))𝜂) ∧ (∀𝑤 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))𝜁 ∧ ∀𝑡 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑢 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))𝜎 ∧ ∀𝑡 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜌) ∧ ∀𝑢 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))𝜇) → 𝜒))

Assertion

Ref	Expression
no3inds	⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → 𝛻)

Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑧,𝛻   𝑦,𝐵,𝑧   𝑧,𝐶   𝜒,𝑝   𝜂,𝑡   𝜅,𝑦   𝜆,𝑥   𝜇,𝑡   𝜓,𝑝   𝑞,𝑝,𝑥,𝑦,𝑧   𝜑,𝑞,𝑥,𝑦,𝑧   𝜓,𝑡,𝑢,𝑤,𝑥,𝑦,𝑧   𝑡,𝑞   𝜃,𝑞,𝑢   𝑤,𝑞,𝑥,𝑦,𝑧   𝜌,𝑢   𝜎,𝑤   𝜏,𝑢   𝑢,𝑡,𝑤,𝑥,𝑦,𝑧   𝜃,𝑢   𝑤,𝑢,𝑥,𝑦,𝑧   𝜁,𝑢   𝑥,𝑤,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑤,𝑢,𝑡,𝑝)   𝜓(𝑞)   𝜒(𝑥,𝑦,𝑧,𝑤,𝑢,𝑡,𝑞)   𝜃(𝑥,𝑦,𝑧,𝑤,𝑡,𝑝)   𝜏(𝑥,𝑦,𝑧,𝑤,𝑡,𝑞,𝑝)   𝜂(𝑥,𝑦,𝑧,𝑤,𝑢,𝑞,𝑝)   𝜁(𝑥,𝑦,𝑧,𝑤,𝑡,𝑞,𝑝)   𝜎(𝑥,𝑦,𝑧,𝑢,𝑡,𝑞,𝑝)   𝜌(𝑥,𝑦,𝑧,𝑤,𝑡,𝑞,𝑝)   𝜇(𝑥,𝑦,𝑧,𝑤,𝑢,𝑞,𝑝)   𝜆(𝑦,𝑧,𝑤,𝑢,𝑡,𝑞,𝑝)   𝜅(𝑥,𝑧,𝑤,𝑢,𝑡,𝑞,𝑝)   𝐴(𝑤,𝑢,𝑡,𝑞,𝑝)   𝐵(𝑥,𝑤,𝑢,𝑡,𝑞,𝑝)   𝐶(𝑥,𝑦,𝑤,𝑢,𝑡,𝑞,𝑝)   𝛻(𝑥,𝑦,𝑤,𝑢,𝑡,𝑞,𝑝)

Proof of Theorem no3inds

Dummy variables 𝑎 𝑏 𝑐 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2758	. 2 ⊢ {⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} = {⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))}
2		eqid 2758	. 2 ⊢ {⟨𝑐, 𝑑⟩ ∣ (𝑐 ∈ (( No × No ) × No ) ∧ 𝑑 ∈ (( No × No ) × No ) ∧ ((((1st ‘(1st ‘𝑐)){⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} (1st ‘(1st ‘𝑑)) ∨ (1st ‘(1st ‘𝑐)) = (1st ‘(1st ‘𝑑))) ∧ ((2nd ‘(1st ‘𝑐)){⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} (2nd ‘(1st ‘𝑑)) ∨ (2nd ‘(1st ‘𝑐)) = (2nd ‘(1st ‘𝑑))) ∧ ((2nd ‘𝑐){⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} (2nd ‘𝑑) ∨ (2nd ‘𝑐) = (2nd ‘𝑑))) ∧ 𝑐 ≠ 𝑑))} = {⟨𝑐, 𝑑⟩ ∣ (𝑐 ∈ (( No × No ) × No ) ∧ 𝑑 ∈ (( No × No ) × No ) ∧ ((((1st ‘(1st ‘𝑐)){⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} (1st ‘(1st ‘𝑑)) ∨ (1st ‘(1st ‘𝑐)) = (1st ‘(1st ‘𝑑))) ∧ ((2nd ‘(1st ‘𝑐)){⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} (2nd ‘(1st ‘𝑑)) ∨ (2nd ‘(1st ‘𝑐)) = (2nd ‘(1st ‘𝑑))) ∧ ((2nd ‘𝑐){⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} (2nd ‘𝑑) ∨ (2nd ‘𝑐) = (2nd ‘𝑑))) ∧ 𝑐 ≠ 𝑑))}
3		no3inds.1	. 2 ⊢ (𝑝 = 𝑞 → (𝜑 ↔ 𝜓))
4		no3inds.2	. 2 ⊢ (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝜑 ↔ 𝜒))
5		no3inds.3	. 2 ⊢ (𝑞 = ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ → (𝜓 ↔ 𝜃))
6		no3inds.4	. 2 ⊢ (𝑢 = 𝑧 → (𝜃 ↔ 𝜏))
7		no3inds.5	. 2 ⊢ (𝑡 = 𝑦 → (𝜃 ↔ 𝜂))
8		no3inds.6	. 2 ⊢ (𝑢 = 𝑧 → (𝜂 ↔ 𝜁))
9		no3inds.7	. 2 ⊢ (𝑤 = 𝑥 → (𝜃 ↔ 𝜎))
10		no3inds.8	. 2 ⊢ (𝑢 = 𝑧 → (𝜎 ↔ 𝜌))
11		no3inds.9	. 2 ⊢ (𝑡 = 𝑦 → (𝜎 ↔ 𝜇))
12		no3inds.10	. 2 ⊢ (𝑥 = 𝐴 → (𝜒 ↔ 𝜆))
13		no3inds.11	. 2 ⊢ (𝑦 = 𝐵 → (𝜆 ↔ 𝜅))
14		no3inds.12	. 2 ⊢ (𝑧 = 𝐶 → (𝜅 ↔ 𝛻))
15		no3inds.i	. 2 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → (((∀𝑤 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑡 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑢 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))𝜃 ∧ ∀𝑤 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑡 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜏 ∧ ∀𝑤 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑢 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))𝜂) ∧ (∀𝑤 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))𝜁 ∧ ∀𝑡 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑢 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))𝜎 ∧ ∀𝑡 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜌) ∧ ∀𝑢 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))𝜇) → 𝜒))
16	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15	no3indslem 33698	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → 𝛻)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070   ∪ cun 3858  ⟨cop 4531   class class class wbr 5036  {copab 5098   × cxp 5526  ‘cfv 6340  1^st c1st 7697  2^nd c2nd 7698   No csur 33441   L cleft 33624   R cright 33625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-1st 7699  df-2nd 7700  df-wrecs 7963  df-recs 8024  df-1o 8118  df-2o 8119  df-no 33444  df-slt 33445  df-bday 33446  df-sslt 33574  df-scut 33576  df-made 33626  df-old 33627  df-left 33629  df-right 33630

This theorem is referenced by: (None)