Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nosupbday Structured version   Visualization version   GIF version

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

Proof of Theorem nosupbday
StepHypRef Expression
1 nosupbday.1 . . . 4 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
21nosupno 31974 . . 3 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
3 bdayval 31926 . . 3 (𝑆 No → ( bday 𝑆) = dom 𝑆)
42, 3syl 17 . 2 ((𝐴 No 𝐴 ∈ V) → ( bday 𝑆) = dom 𝑆)
5 iftrue 4125 . . . . . . . 8 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}))
61, 5syl5eq 2697 . . . . . . 7 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}))
76dmeqd 5358 . . . . . 6 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}))
8 2on 7613 . . . . . . . . . 10 2𝑜 ∈ On
98elexi 3244 . . . . . . . . 9 2𝑜 ∈ V
109dmsnop 5645 . . . . . . . 8 dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩} = {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)}
1110uneq2i 3797 . . . . . . 7 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
12 dmun 5363 . . . . . . 7 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩})
13 df-suc 5767 . . . . . . 7 suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
1411, 12, 133eqtr4i 2683 . . . . . 6 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}) = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
157, 14syl6eq 2701 . . . . 5 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
1615adantr 480 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
17 simprl 809 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → 𝐴 No )
18 simpl 472 . . . . . . . . . . 11 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
19 nomaxmo 31972 . . . . . . . . . . . . 13 (𝐴 No → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
2019adantr 480 . . . . . . . . . . . 12 ((𝐴 No 𝐴 ∈ V) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
2120adantl 481 . . . . . . . . . . 11 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
22 reu5 3189 . . . . . . . . . . 11 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
2318, 21, 22sylanbrc 699 . . . . . . . . . 10 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
24 riotacl 6665 . . . . . . . . . 10 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
2523, 24syl 17 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
2617, 25sseldd 3637 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No )
27 bdayval 31926 . . . . . . . 8 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → ( bday ‘(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
2826, 27syl 17 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ( bday ‘(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
29 bdayfo 31953 . . . . . . . . 9 bday : No onto→On
30 fofn 6155 . . . . . . . . 9 ( bday : No onto→On → bday Fn No )
3129, 30ax-mp 5 . . . . . . . 8 bday Fn No
32 fnfvima 6536 . . . . . . . 8 (( bday Fn No 𝐴 No ∧ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴) → ( bday ‘(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ ( bday 𝐴))
3331, 17, 25, 32mp3an2i 1469 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ( bday ‘(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ ( bday 𝐴))
3428, 33eqeltrrd 2731 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ ( bday 𝐴))
35 elssuni 4499 . . . . . 6 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ ( bday 𝐴) → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ ( bday 𝐴))
3634, 35syl 17 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ ( bday 𝐴))
37 nodmord 31931 . . . . . . 7 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → Ord dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
3826, 37syl 17 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → Ord dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
39 imassrn 5512 . . . . . . . 8 ( bday 𝐴) ⊆ ran bday
40 forn 6156 . . . . . . . . 9 ( bday : No onto→On → ran bday = On)
4129, 40ax-mp 5 . . . . . . . 8 ran bday = On
4239, 41sseqtri 3670 . . . . . . 7 ( bday 𝐴) ⊆ On
43 ssorduni 7027 . . . . . . 7 (( bday 𝐴) ⊆ On → Ord ( bday 𝐴))
4442, 43ax-mp 5 . . . . . 6 Ord ( bday 𝐴)
45 ordsucsssuc 7065 . . . . . 6 ((Ord dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ Ord ( bday 𝐴)) → (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ ( bday 𝐴) ↔ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc ( bday 𝐴)))
4638, 44, 45sylancl 695 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ ( bday 𝐴) ↔ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc ( bday 𝐴)))
4736, 46mpbid 222 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc ( bday 𝐴))
4816, 47eqsstrd 3672 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom 𝑆 ⊆ suc ( bday 𝐴))
49 iffalse 4128 . . . . . . . 8 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
501, 49syl5eq 2697 . . . . . . 7 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
5150dmeqd 5358 . . . . . 6 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
52 iotaex 5906 . . . . . . 7 (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) ∈ V
53 eqid 2651 . . . . . . 7 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
5452, 53dmmpti 6061 . . . . . 6 dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
5551, 54syl6eq 2701 . . . . 5 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
5655adantr 480 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom 𝑆 = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
57 ssel2 3631 . . . . . . . . . . . . . 14 ((𝐴 No 𝑢𝐴) → 𝑢 No )
58 bdayval 31926 . . . . . . . . . . . . . 14 (𝑢 No → ( bday 𝑢) = dom 𝑢)
5957, 58syl 17 . . . . . . . . . . . . 13 ((𝐴 No 𝑢𝐴) → ( bday 𝑢) = dom 𝑢)
60 fnfvima 6536 . . . . . . . . . . . . . 14 (( bday Fn No 𝐴 No 𝑢𝐴) → ( bday 𝑢) ∈ ( bday 𝐴))
6131, 60mp3an1 1451 . . . . . . . . . . . . 13 ((𝐴 No 𝑢𝐴) → ( bday 𝑢) ∈ ( bday 𝐴))
6259, 61eqeltrrd 2731 . . . . . . . . . . . 12 ((𝐴 No 𝑢𝐴) → dom 𝑢 ∈ ( bday 𝐴))
6362adantlr 751 . . . . . . . . . . 11 (((𝐴 No 𝐴 ∈ V) ∧ 𝑢𝐴) → dom 𝑢 ∈ ( bday 𝐴))
64 elssuni 4499 . . . . . . . . . . 11 (dom 𝑢 ∈ ( bday 𝐴) → dom 𝑢 ( bday 𝐴))
6563, 64syl 17 . . . . . . . . . 10 (((𝐴 No 𝐴 ∈ V) ∧ 𝑢𝐴) → dom 𝑢 ( bday 𝐴))
66 sssucid 5840 . . . . . . . . . 10 ( bday 𝐴) ⊆ suc ( bday 𝐴)
6765, 66syl6ss 3648 . . . . . . . . 9 (((𝐴 No 𝐴 ∈ V) ∧ 𝑢𝐴) → dom 𝑢 ⊆ suc ( bday 𝐴))
6867sseld 3635 . . . . . . . 8 (((𝐴 No 𝐴 ∈ V) ∧ 𝑢𝐴) → (𝑦 ∈ dom 𝑢𝑦 ∈ suc ( bday 𝐴)))
6968adantrd 483 . . . . . . 7 (((𝐴 No 𝐴 ∈ V) ∧ 𝑢𝐴) → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ suc ( bday 𝐴)))
7069rexlimdva 3060 . . . . . 6 ((𝐴 No 𝐴 ∈ V) → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ suc ( bday 𝐴)))
7170abssdv 3709 . . . . 5 ((𝐴 No 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ suc ( bday 𝐴))
7271adantl 481 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ suc ( bday 𝐴))
7356, 72eqsstrd 3672 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom 𝑆 ⊆ suc ( bday 𝐴))
7448, 73pm2.61ian 848 . 2 ((𝐴 No 𝐴 ∈ V) → dom 𝑆 ⊆ suc ( bday 𝐴))
754, 74eqsstrd 3672 1 ((𝐴 No 𝐴 ∈ V) → ( bday 𝑆) ⊆ suc ( bday 𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  {cab 2637  ∀wral 2941  ∃wrex 2942  ∃!wreu 2943  ∃*wrmo 2944  Vcvv 3231   ∪ cun 3605   ⊆ wss 3607  ifcif 4119  {csn 4210  ⟨cop 4216  ∪ cuni 4468   class class class wbr 4685   ↦ cmpt 4762  dom cdm 5143  ran crn 5144   ↾ cres 5145   “ cima 5146  Ord word 5760  Oncon0 5761  suc csuc 5763  ℩cio 5887   Fn wfn 5921  –onto→wfo 5924  ‘cfv 5926  ℩crio 6650  2𝑜c2o 7599   No csur 31918
 Copyright terms: Public domain W3C validator