MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nosupbday Structured version   Visualization version   GIF version

Theorem nosupbday 27765
Description: Birthday bounding law for surreal supremum. (Contributed by Scott Fenton, 5-Dec-2021.)
Hypothesis
Ref Expression
nosupbday.1 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
Assertion
Ref Expression
nosupbday (((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) → ( bday 𝑆) ⊆ 𝑂)
Distinct variable groups:   𝐴,𝑔,𝑢,𝑣,𝑥,𝑦   𝑢,𝑂,𝑦
Allowed substitution hints:   𝑆(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑂(𝑥,𝑣,𝑔)

Proof of Theorem nosupbday
StepHypRef Expression
1 nosupbday.1 . . . . 5 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
21nosupno 27763 . . . 4 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
32adantr 480 . . 3 (((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) → 𝑆 No )
4 bdayval 27708 . . 3 (𝑆 No → ( bday 𝑆) = dom 𝑆)
53, 4syl 17 . 2 (((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) → ( bday 𝑆) = dom 𝑆)
6 iftrue 4537 . . . . . . . 8 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
71, 6eqtrid 2787 . . . . . . 7 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
87dmeqd 5919 . . . . . 6 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
9 2oex 8516 . . . . . . . . 9 2o ∈ V
109dmsnop 6238 . . . . . . . 8 dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩} = {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)}
1110uneq2i 4175 . . . . . . 7 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
12 dmun 5924 . . . . . . 7 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})
13 df-suc 6392 . . . . . . 7 suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
1411, 12, 133eqtr4i 2773 . . . . . 6 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
158, 14eqtrdi 2791 . . . . 5 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
1615adantr 480 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
17 simprrl 781 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → 𝑂 ∈ On)
18 eloni 6396 . . . . . 6 (𝑂 ∈ On → Ord 𝑂)
1917, 18syl 17 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → Ord 𝑂)
20 simprll 779 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → 𝐴 No )
21 simpl 482 . . . . . . . . . . 11 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
22 nomaxmo 27758 . . . . . . . . . . . . 13 (𝐴 No → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
2322adantr 480 . . . . . . . . . . . 12 ((𝐴 No 𝐴 ∈ V) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
2423adantl 481 . . . . . . . . . . 11 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
25 reu5 3380 . . . . . . . . . . 11 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
2621, 24, 25sylanbrc 583 . . . . . . . . . 10 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
2726adantrr 717 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
28 riotacl 7405 . . . . . . . . 9 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
2927, 28syl 17 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
3020, 29sseldd 3996 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No )
31 bdayval 27708 . . . . . . 7 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → ( bday ‘(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
3230, 31syl 17 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → ( bday ‘(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
33 simprrr 782 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → ( bday 𝐴) ⊆ 𝑂)
34 bdayfo 27737 . . . . . . . . 9 bday : No onto→On
35 fofn 6823 . . . . . . . . 9 ( bday : No onto→On → bday Fn No )
3634, 35ax-mp 5 . . . . . . . 8 bday Fn No
37 fnfvima 7253 . . . . . . . 8 (( bday Fn No 𝐴 No ∧ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴) → ( bday ‘(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ ( bday 𝐴))
3836, 20, 29, 37mp3an2i 1465 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → ( bday ‘(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ ( bday 𝐴))
3933, 38sseldd 3996 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → ( bday ‘(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ 𝑂)
4032, 39eqeltrrd 2840 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝑂)
41 ordsucss 7838 . . . . 5 (Ord 𝑂 → (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝑂 → suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ 𝑂))
4219, 40, 41sylc 65 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ 𝑂)
4316, 42eqsstrd 4034 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → dom 𝑆𝑂)
44 iffalse 4540 . . . . . . . 8 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
451, 44eqtrid 2787 . . . . . . 7 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
4645dmeqd 5919 . . . . . 6 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
47 iotaex 6536 . . . . . . 7 (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) ∈ V
48 eqid 2735 . . . . . . 7 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
4947, 48dmmpti 6713 . . . . . 6 dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
5046, 49eqtrdi 2791 . . . . 5 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
5150adantr 480 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → dom 𝑆 = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
52 simplrl 777 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) ∧ 𝑢𝐴) → 𝑂 ∈ On)
53 ssel2 3990 . . . . . . . . . . . . 13 ((𝐴 No 𝑢𝐴) → 𝑢 No )
5453ad4ant14 752 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) ∧ 𝑢𝐴) → 𝑢 No )
55 bdayval 27708 . . . . . . . . . . . 12 (𝑢 No → ( bday 𝑢) = dom 𝑢)
5654, 55syl 17 . . . . . . . . . . 11 ((((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) ∧ 𝑢𝐴) → ( bday 𝑢) = dom 𝑢)
57 simplrr 778 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) ∧ 𝑢𝐴) → ( bday 𝐴) ⊆ 𝑂)
58 fnfvima 7253 . . . . . . . . . . . . . 14 (( bday Fn No 𝐴 No 𝑢𝐴) → ( bday 𝑢) ∈ ( bday 𝐴))
5936, 58mp3an1 1447 . . . . . . . . . . . . 13 ((𝐴 No 𝑢𝐴) → ( bday 𝑢) ∈ ( bday 𝐴))
6059ad4ant14 752 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) ∧ 𝑢𝐴) → ( bday 𝑢) ∈ ( bday 𝐴))
6157, 60sseldd 3996 . . . . . . . . . . 11 ((((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) ∧ 𝑢𝐴) → ( bday 𝑢) ∈ 𝑂)
6256, 61eqeltrrd 2840 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) ∧ 𝑢𝐴) → dom 𝑢𝑂)
63 onelss 6428 . . . . . . . . . 10 (𝑂 ∈ On → (dom 𝑢𝑂 → dom 𝑢𝑂))
6452, 62, 63sylc 65 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) ∧ 𝑢𝐴) → dom 𝑢𝑂)
6564sseld 3994 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) ∧ 𝑢𝐴) → (𝑦 ∈ dom 𝑢𝑦𝑂))
6665adantrd 491 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) ∧ 𝑢𝐴) → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦𝑂))
6766rexlimdva 3153 . . . . . 6 (((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦𝑂))
6867abssdv 4078 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ 𝑂)
6968adantl 481 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ 𝑂)
7051, 69eqsstrd 4034 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂))) → dom 𝑆𝑂)
7143, 70pm2.61ian 812 . 2 (((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) → dom 𝑆𝑂)
725, 71eqsstrd 4034 1 (((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) → ( bday 𝑆) ⊆ 𝑂)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  w3a 1086   = wceq 1537  wcel 2106  {cab 2712  wral 3059  wrex 3068  ∃!wreu 3376  ∃*wrmo 3377  Vcvv 3478  cun 3961  wss 3963  ifcif 4531  {csn 4631  cop 4637   class class class wbr 5148  cmpt 5231  dom cdm 5689  cres 5691  cima 5692  Ord word 6385  Oncon0 6386  suc csuc 6388  cio 6514   Fn wfn 6558  ontowfo 6561  cfv 6563  crio 7387  2oc2o 8499   No csur 27699   <s cslt 27700   bday cbday 27701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-ord 6389  df-on 6390  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fo 6569  df-fv 6571  df-riota 7388  df-1o 8505  df-2o 8506  df-no 27702  df-slt 27703  df-bday 27704
This theorem is referenced by:  noetalem1  27801
  Copyright terms: Public domain W3C validator