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

Theorem nosupbday 32766
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) → ( bday 𝑆) ⊆ suc ( bday 𝐴))
Distinct variable group:   𝐴,𝑔,𝑢,𝑣,𝑥,𝑦
Allowed substitution hints:   𝑆(𝑥,𝑦,𝑣,𝑢,𝑔)

Proof of Theorem nosupbday
StepHypRef Expression
1 nosupbday.1 . . . 4 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
21nosupno 32764 . . 3 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
3 bdayval 32716 . . 3 (𝑆 No → ( bday 𝑆) = dom 𝑆)
42, 3syl 17 . 2 ((𝐴 No 𝐴 ∈ V) → ( bday 𝑆) = dom 𝑆)
5 iftrue 4359 . . . . . . . 8 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
61, 5syl5eq 2828 . . . . . . 7 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
76dmeqd 5628 . . . . . 6 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
8 2on 7920 . . . . . . . . . 10 2o ∈ On
98elexi 3436 . . . . . . . . 9 2o ∈ V
109dmsnop 5917 . . . . . . . 8 dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩} = {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)}
1110uneq2i 4027 . . . . . . 7 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
12 dmun 5633 . . . . . . 7 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})
13 df-suc 6040 . . . . . . 7 suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
1411, 12, 133eqtr4i 2814 . . . . . 6 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
157, 14syl6eq 2832 . . . . 5 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
1615adantr 473 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
17 simprl 759 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → 𝐴 No )
18 simpl 475 . . . . . . . . . . 11 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
19 nomaxmo 32762 . . . . . . . . . . . . 13 (𝐴 No → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
2019adantr 473 . . . . . . . . . . . 12 ((𝐴 No 𝐴 ∈ V) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
2120adantl 474 . . . . . . . . . . 11 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
22 reu5 3372 . . . . . . . . . . 11 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
2318, 21, 22sylanbrc 575 . . . . . . . . . 10 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
24 riotacl 6957 . . . . . . . . . 10 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
2523, 24syl 17 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
2617, 25sseldd 3861 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No )
27 bdayval 32716 . . . . . . . 8 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → ( bday ‘(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
2826, 27syl 17 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ( bday ‘(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
29 bdayfo 32743 . . . . . . . . 9 bday : No onto→On
30 fofn 6426 . . . . . . . . 9 ( bday : No onto→On → bday Fn No )
3129, 30ax-mp 5 . . . . . . . 8 bday Fn No
32 fnfvima 6826 . . . . . . . 8 (( bday Fn No 𝐴 No ∧ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴) → ( bday ‘(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ ( bday 𝐴))
3331, 17, 25, 32mp3an2i 1446 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ( bday ‘(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ ( bday 𝐴))
3428, 33eqeltrrd 2869 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ ( bday 𝐴))
35 elssuni 4746 . . . . . 6 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ ( bday 𝐴) → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ ( bday 𝐴))
3634, 35syl 17 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ ( bday 𝐴))
37 nodmord 32721 . . . . . . 7 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → Ord dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
3826, 37syl 17 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → Ord dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
39 imassrn 5786 . . . . . . . 8 ( bday 𝐴) ⊆ ran bday
40 forn 6427 . . . . . . . . 9 ( bday : No onto→On → ran bday = On)
4129, 40ax-mp 5 . . . . . . . 8 ran bday = On
4239, 41sseqtri 3895 . . . . . . 7 ( bday 𝐴) ⊆ On
43 ssorduni 7322 . . . . . . 7 (( bday 𝐴) ⊆ On → Ord ( bday 𝐴))
4442, 43ax-mp 5 . . . . . 6 Ord ( bday 𝐴)
45 ordsucsssuc 7360 . . . . . 6 ((Ord dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ Ord ( bday 𝐴)) → (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ ( bday 𝐴) ↔ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc ( bday 𝐴)))
4638, 44, 45sylancl 578 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ ( bday 𝐴) ↔ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc ( bday 𝐴)))
4736, 46mpbid 224 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc ( bday 𝐴))
4816, 47eqsstrd 3897 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom 𝑆 ⊆ suc ( bday 𝐴))
49 iffalse 4362 . . . . . . . 8 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
501, 49syl5eq 2828 . . . . . . 7 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
5150dmeqd 5628 . . . . . 6 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
52 iotaex 6174 . . . . . . 7 (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) ∈ V
53 eqid 2780 . . . . . . 7 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
5452, 53dmmpti 6327 . . . . . 6 dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
5551, 54syl6eq 2832 . . . . 5 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
5655adantr 473 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom 𝑆 = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
57 ssel2 3855 . . . . . . . . . . . . . 14 ((𝐴 No 𝑢𝐴) → 𝑢 No )
58 bdayval 32716 . . . . . . . . . . . . . 14 (𝑢 No → ( bday 𝑢) = dom 𝑢)
5957, 58syl 17 . . . . . . . . . . . . 13 ((𝐴 No 𝑢𝐴) → ( bday 𝑢) = dom 𝑢)
60 fnfvima 6826 . . . . . . . . . . . . . 14 (( bday Fn No 𝐴 No 𝑢𝐴) → ( bday 𝑢) ∈ ( bday 𝐴))
6131, 60mp3an1 1428 . . . . . . . . . . . . 13 ((𝐴 No 𝑢𝐴) → ( bday 𝑢) ∈ ( bday 𝐴))
6259, 61eqeltrrd 2869 . . . . . . . . . . . 12 ((𝐴 No 𝑢𝐴) → dom 𝑢 ∈ ( bday 𝐴))
6362adantlr 703 . . . . . . . . . . 11 (((𝐴 No 𝐴 ∈ V) ∧ 𝑢𝐴) → dom 𝑢 ∈ ( bday 𝐴))
64 elssuni 4746 . . . . . . . . . . 11 (dom 𝑢 ∈ ( bday 𝐴) → dom 𝑢 ( bday 𝐴))
6563, 64syl 17 . . . . . . . . . 10 (((𝐴 No 𝐴 ∈ V) ∧ 𝑢𝐴) → dom 𝑢 ( bday 𝐴))
66 sssucid 6111 . . . . . . . . . 10 ( bday 𝐴) ⊆ suc ( bday 𝐴)
6765, 66syl6ss 3872 . . . . . . . . 9 (((𝐴 No 𝐴 ∈ V) ∧ 𝑢𝐴) → dom 𝑢 ⊆ suc ( bday 𝐴))
6867sseld 3859 . . . . . . . 8 (((𝐴 No 𝐴 ∈ V) ∧ 𝑢𝐴) → (𝑦 ∈ dom 𝑢𝑦 ∈ suc ( bday 𝐴)))
6968adantrd 484 . . . . . . 7 (((𝐴 No 𝐴 ∈ V) ∧ 𝑢𝐴) → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ suc ( bday 𝐴)))
7069rexlimdva 3231 . . . . . 6 ((𝐴 No 𝐴 ∈ V) → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ suc ( bday 𝐴)))
7170abssdv 3937 . . . . 5 ((𝐴 No 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ suc ( bday 𝐴))
7271adantl 474 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ suc ( bday 𝐴))
7356, 72eqsstrd 3897 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom 𝑆 ⊆ suc ( bday 𝐴))
7448, 73pm2.61ian 800 . 2 ((𝐴 No 𝐴 ∈ V) → dom 𝑆 ⊆ suc ( bday 𝐴))
754, 74eqsstrd 3897 1 ((𝐴 No 𝐴 ∈ V) → ( bday 𝑆) ⊆ suc ( bday 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  w3a 1069   = wceq 1508  wcel 2051  {cab 2760  wral 3090  wrex 3091  ∃!wreu 3092  ∃*wrmo 3093  Vcvv 3417  cun 3829  wss 3831  ifcif 4353  {csn 4444  cop 4450   cuni 4717   class class class wbr 4934  cmpt 5013  dom cdm 5411  ran crn 5412  cres 5413  cima 5414  Ord word 6033  Oncon0 6034  suc csuc 6036  cio 6155   Fn wfn 6188  ontowfo 6191  cfv 6193  crio 6942  2oc2o 7905   No csur 32708   <s cslt 32709   bday cbday 32710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2752  ax-rep 5053  ax-sep 5064  ax-nul 5071  ax-pow 5123  ax-pr 5190  ax-un 7285
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2551  df-eu 2589  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3419  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4182  df-if 4354  df-pw 4427  df-sn 4445  df-pr 4447  df-tp 4449  df-op 4451  df-uni 4718  df-iun 4799  df-br 4935  df-opab 4997  df-mpt 5014  df-tr 5036  df-id 5316  df-eprel 5321  df-po 5330  df-so 5331  df-fr 5370  df-we 5372  df-xp 5417  df-rel 5418  df-cnv 5419  df-co 5420  df-dm 5421  df-rn 5422  df-res 5423  df-ima 5424  df-ord 6037  df-on 6038  df-suc 6040  df-iota 6157  df-fun 6195  df-fn 6196  df-f 6197  df-f1 6198  df-fo 6199  df-f1o 6200  df-fv 6201  df-riota 6943  df-1o 7911  df-2o 7912  df-no 32711  df-slt 32712  df-bday 32713
This theorem is referenced by:  noetalem4  32781
  Copyright terms: Public domain W3C validator