Theorem noetasuplem1 33533

Description: Lemma for noeta 33543. Establish that our final surreal really is a surreal. (Contributed by Scott Fenton, 6-Dec-2021.)

Hypotheses

Ref	Expression
noetasuplem.1	⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
noetasuplem.2	⊢ 𝑍 = (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}))

Assertion

Ref	Expression
noetasuplem1	⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑍 ∈ No )

Distinct variable group:   𝐴,𝑔,𝑢,𝑣,𝑥,𝑦

Allowed substitution hints:   𝐵(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑆(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑍(𝑥,𝑦,𝑣,𝑢,𝑔)

Proof of Theorem noetasuplem1

Step	Hyp	Ref	Expression
1		noetasuplem.2	. 2 ⊢ 𝑍 = (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}))
2		noetasuplem.1	. . . . 5 ⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
3	2	nosupno 33503	. . . 4 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → 𝑆 ∈ No )
4	3	3adant3 1129	. . 3 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑆 ∈ No )
5		bdayimaon 33493	. . . 4 ⊢ (𝐵 ∈ V → suc ∪ ( bday “ 𝐵) ∈ On)
6	5	3ad2ant3 1132	. . 3 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) → suc ∪ ( bday “ 𝐵) ∈ On)
7		1oex 8126	. . . . 5 ⊢ 1o ∈ V
8	7	prid1 4658	. . . 4 ⊢ 1o ∈ {1o, 2o}
9	8	noextendseq 33467	. . 3 ⊢ ((𝑆 ∈ No ∧ suc ∪ ( bday “ 𝐵) ∈ On) → (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})) ∈ No )
10	4, 6, 9	syl2anc 587	. 2 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})) ∈ No )
11	1, 10	eqeltrid 2856	1 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑍 ∈ No )

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {cab 2735  ∀wral 3070  ∃wrex 3071  Vcvv 3409   ∖ cdif 3857   ∪ cun 3858   ⊆ wss 3860  ifcif 4423  {csn 4525  ⟨cop 4531  ∪ cuni 4801   class class class wbr 5036   ↦ cmpt 5116   × cxp 5526  dom cdm 5528   ↾ cres 5530   “ cima 5531  Oncon0 6174  suc csuc 6176  ℩cio 6297  ‘cfv 6340  ℩crio 7113  1_oc1o 8111  2_oc2o 8112   No csur 33440   <s cslt 33441   bday cbday 33442

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-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-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-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-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-1o 8118  df-2o 8119  df-no 33443  df-slt 33444  df-bday 33445

This theorem is referenced by:  noetasuplem3  33535  noetasuplem4  33536  noetalem1  33541