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

Theorem noinfbday 33488
 Description: Birthday bounding law for surreal infimum. (Contributed by Scott Fenton, 8-Aug-2024.)
Hypothesis
Ref Expression
noinfbday.1 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
Assertion
Ref Expression
noinfbday (((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) → ( bday 𝑇) ⊆ 𝑂)
Distinct variable groups:   𝐵,𝑔,𝑢,𝑣,𝑥,𝑦   𝑔,𝑉   𝑥,𝑣,𝑦
Allowed substitution hints:   𝑇(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑂(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑉(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem noinfbday
Dummy variables 𝑝 𝑞 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 noinfbday.1 . . . . 5 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
21noinfno 33486 . . . 4 ((𝐵 No 𝐵𝑉) → 𝑇 No )
3 bdayval 33416 . . . 4 (𝑇 No → ( bday 𝑇) = dom 𝑇)
42, 3syl 17 . . 3 ((𝐵 No 𝐵𝑉) → ( bday 𝑇) = dom 𝑇)
54adantr 484 . 2 (((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) → ( bday 𝑇) = dom 𝑇)
6 iftrue 4426 . . . . . . . 8 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
71, 6syl5eq 2805 . . . . . . 7 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥𝑇 = ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
87dmeqd 5745 . . . . . 6 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
9 1oex 8120 . . . . . . . . 9 1o ∈ V
109dmsnop 6045 . . . . . . . 8 dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩} = {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)}
1110uneq2i 4065 . . . . . . 7 (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)})
12 dmun 5750 . . . . . . 7 dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩})
13 df-suc 6175 . . . . . . 7 suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)})
1411, 12, 133eqtr4i 2791 . . . . . 6 dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
158, 14eqtrdi 2809 . . . . 5 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
1615adantr 484 . . . 4 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → dom 𝑇 = suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
17 simprrl 780 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → 𝑂 ∈ On)
18 eloni 6179 . . . . . 6 (𝑂 ∈ On → Ord 𝑂)
1917, 18syl 17 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → Ord 𝑂)
20 simprll 778 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → 𝐵 No )
21 simpl 486 . . . . . . . . . 10 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
22 nominmo 33467 . . . . . . . . . . 11 (𝐵 No → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2320, 22syl 17 . . . . . . . . . 10 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
24 reu5 3340 . . . . . . . . . 10 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
2521, 23, 24sylanbrc 586 . . . . . . . . 9 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
26 riotacl 7125 . . . . . . . . 9 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵)
2725, 26syl 17 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵)
2820, 27sseldd 3893 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No )
29 bdayval 33416 . . . . . . 7 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No → ( bday ‘(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) = dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
3028, 29syl 17 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → ( bday ‘(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) = dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
31 simprrr 781 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → ( bday 𝐵) ⊆ 𝑂)
32 bdayfo 33445 . . . . . . . . 9 bday : No onto→On
33 fofn 6578 . . . . . . . . 9 ( bday : No onto→On → bday Fn No )
3432, 33ax-mp 5 . . . . . . . 8 bday Fn No
35 fnfvima 6987 . . . . . . . 8 (( bday Fn No 𝐵 No ∧ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵) → ( bday ‘(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ∈ ( bday 𝐵))
3634, 20, 27, 35mp3an2i 1463 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → ( bday ‘(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ∈ ( bday 𝐵))
3731, 36sseldd 3893 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → ( bday ‘(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ∈ 𝑂)
3830, 37eqeltrrd 2853 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝑂)
39 ordsucss 7532 . . . . 5 (Ord 𝑂 → (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝑂 → suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ⊆ 𝑂))
4019, 38, 39sylc 65 . . . 4 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ⊆ 𝑂)
4116, 40eqsstrd 3930 . . 3 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → dom 𝑇𝑂)
421noinfdm 33487 . . . . 5 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑧 ∣ ∃𝑝𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))})
4342adantr 484 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → dom 𝑇 = {𝑧 ∣ ∃𝑝𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))})
44 simplrl 776 . . . . . . . . . . 11 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → 𝑂 ∈ On)
4544, 18syl 17 . . . . . . . . . 10 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → Ord 𝑂)
46 ssel2 3887 . . . . . . . . . . . . 13 ((𝐵 No 𝑝𝐵) → 𝑝 No )
4746ad4ant14 751 . . . . . . . . . . . 12 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → 𝑝 No )
48 bdayval 33416 . . . . . . . . . . . 12 (𝑝 No → ( bday 𝑝) = dom 𝑝)
4947, 48syl 17 . . . . . . . . . . 11 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → ( bday 𝑝) = dom 𝑝)
50 simplrr 777 . . . . . . . . . . . 12 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → ( bday 𝐵) ⊆ 𝑂)
51 fnfvima 6987 . . . . . . . . . . . . . 14 (( bday Fn No 𝐵 No 𝑝𝐵) → ( bday 𝑝) ∈ ( bday 𝐵))
5234, 51mp3an1 1445 . . . . . . . . . . . . 13 ((𝐵 No 𝑝𝐵) → ( bday 𝑝) ∈ ( bday 𝐵))
5352ad4ant14 751 . . . . . . . . . . . 12 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → ( bday 𝑝) ∈ ( bday 𝐵))
5450, 53sseldd 3893 . . . . . . . . . . 11 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → ( bday 𝑝) ∈ 𝑂)
5549, 54eqeltrrd 2853 . . . . . . . . . 10 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → dom 𝑝𝑂)
56 ordelss 6185 . . . . . . . . . 10 ((Ord 𝑂 ∧ dom 𝑝𝑂) → dom 𝑝𝑂)
5745, 55, 56syl2anc 587 . . . . . . . . 9 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → dom 𝑝𝑂)
5857sseld 3891 . . . . . . . 8 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → (𝑧 ∈ dom 𝑝𝑧𝑂))
5958adantrd 495 . . . . . . 7 ((((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) ∧ 𝑝𝐵) → ((𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))) → 𝑧𝑂))
6059rexlimdva 3208 . . . . . 6 (((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) → (∃𝑝𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))) → 𝑧𝑂))
6160abssdv 3973 . . . . 5 (((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) → {𝑧 ∣ ∃𝑝𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))} ⊆ 𝑂)
6261adantl 485 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → {𝑧 ∣ ∃𝑝𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))} ⊆ 𝑂)
6343, 62eqsstrd 3930 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂))) → dom 𝑇𝑂)
6441, 63pm2.61ian 811 . 2 (((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) → dom 𝑇𝑂)
655, 64eqsstrd 3930 1 (((𝐵 No 𝐵𝑉) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) → ( bday 𝑇) ⊆ 𝑂)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {cab 2735  ∀wral 3070  ∃wrex 3071  ∃!wreu 3072  ∃*wrmo 3073   ∪ cun 3856   ⊆ wss 3858  ifcif 4420  {csn 4522  ⟨cop 4528   class class class wbr 5032   ↦ cmpt 5112  dom cdm 5524   ↾ cres 5526   “ cima 5527  Ord word 6168  Oncon0 6169  suc csuc 6171  ℩cio 6292   Fn wfn 6330  –onto→wfo 6333  ‘cfv 6335  ℩crio 7107  1oc1o 8105   No csur 33408
 Copyright terms: Public domain W3C validator