Metamath Proof Explorer

Theorem noinfbday

Description: Birthday bounding law for surreal infimum. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Hypothesis noinfbday.1 ⊢ T = if ∃ x ∈ B ∀ y ∈ B ¬ y < s x ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 g ∈ y | ∃ u ∈ B y ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ B g ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x
Assertion noinfbday ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → bday ⁡ T ⊆ O

Proof

Step Hyp Ref Expression
1 noinfbday.1 ⊢ T = if ∃ x ∈ B ∀ y ∈ B ¬ y < s x ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 g ∈ y | ∃ u ∈ B y ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ B g ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x
2 1 noinfno ⊢ B ⊆ No ∧ B ∈ V → T ∈ No
3 bdayval ⊢ T ∈ No → bday ⁡ T = dom ⁡ T
4 2 3 syl ⊢ B ⊆ No ∧ B ∈ V → bday ⁡ T = dom ⁡ T
5 4 adantr ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → bday ⁡ T = dom ⁡ T
6 iftrue ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x → if ∃ x ∈ B ∀ y ∈ B ¬ y < s x ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 g ∈ y | ∃ u ∈ B y ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ B g ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x = ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜
7 1 6 syl5eq ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x → T = ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜
8 7 dmeqd ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x → dom ⁡ T = dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜
9 1oex ⊢ 1 𝑜 ∈ V
10 9 dmsnop ⊢ dom ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 = dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
11 10 uneq2i ⊢ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 = dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
12 dmun ⊢ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 = dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜
13 df-suc ⊢ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x = dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
14 11 12 13 3eqtr4i ⊢ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 = suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
15 8 14 eqtrdi ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x → dom ⁡ T = suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
16 15 adantr ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → dom ⁡ T = suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
17 simprrl ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → O ∈ On
18 eloni ⊢ O ∈ On → Ord ⁡ O
19 17 18 syl ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → Ord ⁡ O
20 simprll ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → B ⊆ No
21 simpl ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → ∃ x ∈ B ∀ y ∈ B ¬ y < s x
22 nominmo ⊢ B ⊆ No → ∃* x ∈ B ∀ y ∈ B ¬ y < s x
23 20 22 syl ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → ∃* x ∈ B ∀ y ∈ B ¬ y < s x
24 reu5 ⊢ ∃! x ∈ B ∀ y ∈ B ¬ y < s x ↔ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ ∃* x ∈ B ∀ y ∈ B ¬ y < s x
25 21 23 24 sylanbrc ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → ∃! x ∈ B ∀ y ∈ B ¬ y < s x
26 riotacl ⊢ ∃! x ∈ B ∀ y ∈ B ¬ y < s x → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ B
27 25 26 syl ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ B
28 20 27 sseldd ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ No
29 bdayval ⊢ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ No → bday ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x = dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
30 28 29 syl ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → bday ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x = dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
31 simprrr ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → bday B ⊆ O
32 bdayfo ⊢ bday : No ⟶ onto On
33 fofn ⊢ bday : No ⟶ onto On → bday Fn No
34 32 33 ax-mp ⊢ bday Fn No
35 fnfvima ⊢ bday Fn No ∧ B ⊆ No ∧ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ B → bday ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ bday B
36 34 20 27 35 mp3an2i ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → bday ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ bday B
37 31 36 sseldd ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → bday ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ O
38 30 37 eqeltrrd ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ O
39 ordsucss ⊢ Ord ⁡ O → dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ O → suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ⊆ O
40 19 38 39 sylc ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ⊆ O
41 16 40 eqsstrd ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → dom ⁡ T ⊆ O
42 1 noinfdm ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x → dom ⁡ T = z | ∃ p ∈ B z ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ z = q ↾ suc ⁡ z
43 42 adantr ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → dom ⁡ T = z | ∃ p ∈ B z ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ z = q ↾ suc ⁡ z
44 simplrl ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O ∧ p ∈ B → O ∈ On
45 44 18 syl ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O ∧ p ∈ B → Ord ⁡ O
46 ssel2 ⊢ B ⊆ No ∧ p ∈ B → p ∈ No
47 46 ad4ant14 ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O ∧ p ∈ B → p ∈ No
48 bdayval ⊢ p ∈ No → bday ⁡ p = dom ⁡ p
49 47 48 syl ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O ∧ p ∈ B → bday ⁡ p = dom ⁡ p
50 simplrr ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O ∧ p ∈ B → bday B ⊆ O
51 fnfvima ⊢ bday Fn No ∧ B ⊆ No ∧ p ∈ B → bday ⁡ p ∈ bday B
52 34 51 mp3an1 ⊢ B ⊆ No ∧ p ∈ B → bday ⁡ p ∈ bday B
53 52 ad4ant14 ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O ∧ p ∈ B → bday ⁡ p ∈ bday B
54 50 53 sseldd ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O ∧ p ∈ B → bday ⁡ p ∈ O
55 49 54 eqeltrrd ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O ∧ p ∈ B → dom ⁡ p ∈ O
56 ordelss ⊢ Ord ⁡ O ∧ dom ⁡ p ∈ O → dom ⁡ p ⊆ O
57 45 55 56 syl2anc ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O ∧ p ∈ B → dom ⁡ p ⊆ O
58 57 sseld ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O ∧ p ∈ B → z ∈ dom ⁡ p → z ∈ O
59 58 adantrd ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O ∧ p ∈ B → z ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ z = q ↾ suc ⁡ z → z ∈ O
60 59 rexlimdva ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → ∃ p ∈ B z ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ z = q ↾ suc ⁡ z → z ∈ O
61 60 abssdv ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → z | ∃ p ∈ B z ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ z = q ↾ suc ⁡ z ⊆ O
62 61 adantl ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → z | ∃ p ∈ B z ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ z = q ↾ suc ⁡ z ⊆ O
63 43 62 eqsstrd ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → dom ⁡ T ⊆ O
64 41 63 pm2.61ian ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → dom ⁡ T ⊆ O
65 5 64 eqsstrd ⊢ B ⊆ No ∧ B ∈ V ∧ O ∈ On ∧ bday B ⊆ O → bday ⁡ T ⊆ O