Metamath Proof Explorer

Theorem noinfbnd1

Description: Bounding law from above for the surreal infimum. Analagous to proposition 4.2 of Lipparini p. 6. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis noinfbnd1.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 noinfbnd1 ⊢ B ⊆ No ∧ B ∈ V ∧ U ∈ B → T < s U ↾ dom ⁡ T

Proof

Step Hyp Ref Expression
1 noinfbnd1.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 simpr1 ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → B ⊆ No
3 simpl ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ∃ x ∈ B ∀ y ∈ B ¬ y < s x
4 nominmo ⊢ B ⊆ No → ∃* x ∈ B ∀ y ∈ B ¬ y < s x
5 2 4 syl ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ∃* x ∈ B ∀ y ∈ B ¬ y < s x
6 reu5 ⊢ ∃! x ∈ B ∀ y ∈ B ¬ y < s x ↔ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ ∃* x ∈ B ∀ y ∈ B ¬ y < s x
7 3 5 6 sylanbrc ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ∃! x ∈ B ∀ y ∈ B ¬ y < s x
8 riotacl ⊢ ∃! x ∈ B ∀ y ∈ B ¬ y < s x → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ B
9 7 8 syl ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ B
10 2 9 sseldd ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ No
11 noextendlt ⊢ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ No → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
12 10 11 syl ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
13 simpr3 ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → U ∈ B
14 nfv ⊢ Ⅎ x B ⊆ No ∧ B ∈ V ∧ U ∈ B
15 nfcv ⊢ Ⅎ _ x B
16 nfcv ⊢ Ⅎ _ x y
17 nfcv ⊢ Ⅎ _ x < s
18 nfriota1 ⊢ Ⅎ _ x ι x ∈ B | ∀ y ∈ B ¬ y < s x
19 16 17 18 nfbr ⊢ Ⅎ x y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
20 19 nfn ⊢ Ⅎ x ¬ y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
21 15 20 nfralw ⊢ Ⅎ x ∀ y ∈ B ¬ y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
22 14 21 nfim ⊢ Ⅎ x B ⊆ No ∧ B ∈ V ∧ U ∈ B → ∀ y ∈ B ¬ y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
23 simpl ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → x ∈ B ∧ ∀ y ∈ B ¬ y < s x
24 rspe ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x → ∃ x ∈ B ∀ y ∈ B ¬ y < s x
25 24 adantr ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ∃ x ∈ B ∀ y ∈ B ¬ y < s x
26 simpr1 ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → B ⊆ No
27 26 4 syl ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ∃* x ∈ B ∀ y ∈ B ¬ y < s x
28 25 27 6 sylanbrc ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ∃! x ∈ B ∀ y ∈ B ¬ y < s x
29 riota1 ⊢ ∃! x ∈ B ∀ y ∈ B ¬ y < s x → x ∈ B ∧ ∀ y ∈ B ¬ y < s x ↔ ι x ∈ B | ∀ y ∈ B ¬ y < s x = x
30 28 29 syl ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → x ∈ B ∧ ∀ y ∈ B ¬ y < s x ↔ ι x ∈ B | ∀ y ∈ B ¬ y < s x = x
31 23 30 mpbid ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ι x ∈ B | ∀ y ∈ B ¬ y < s x = x
32 simplr ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ∀ y ∈ B ¬ y < s x
33 nfra1 ⊢ Ⅎ y ∀ y ∈ B ¬ y < s x
34 nfcv ⊢ Ⅎ _ y B
35 33 34 nfriota ⊢ Ⅎ _ y ι x ∈ B | ∀ y ∈ B ¬ y < s x
36 35 nfeq1 ⊢ Ⅎ y ι x ∈ B | ∀ y ∈ B ¬ y < s x = x
37 breq2 ⊢ ι x ∈ B | ∀ y ∈ B ¬ y < s x = x → y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x ↔ y < s x
38 37 notbid ⊢ ι x ∈ B | ∀ y ∈ B ¬ y < s x = x → ¬ y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x ↔ ¬ y < s x
39 36 38 ralbid ⊢ ι x ∈ B | ∀ y ∈ B ¬ y < s x = x → ∀ y ∈ B ¬ y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x ↔ ∀ y ∈ B ¬ y < s x
40 39 biimprd ⊢ ι x ∈ B | ∀ y ∈ B ¬ y < s x = x → ∀ y ∈ B ¬ y < s x → ∀ y ∈ B ¬ y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
41 31 32 40 sylc ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ∀ y ∈ B ¬ y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
42 41 exp31 ⊢ x ∈ B → ∀ y ∈ B ¬ y < s x → B ⊆ No ∧ B ∈ V ∧ U ∈ B → ∀ y ∈ B ¬ y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
43 22 42 rexlimi ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x → B ⊆ No ∧ B ∈ V ∧ U ∈ B → ∀ y ∈ B ¬ y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
44 43 imp ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ∀ y ∈ B ¬ y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
45 nfcv ⊢ Ⅎ _ y U
46 nfcv ⊢ Ⅎ _ y < s
47 45 46 35 nfbr ⊢ Ⅎ y U < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
48 47 nfn ⊢ Ⅎ y ¬ U < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
49 breq1 ⊢ y = U → y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x ↔ U < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
50 49 notbid ⊢ y = U → ¬ y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x ↔ ¬ U < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
51 48 50 rspc ⊢ U ∈ B → ∀ y ∈ B ¬ y < s ι x ∈ B | ∀ y ∈ B ¬ y < s x → ¬ U < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
52 13 44 51 sylc ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ¬ U < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
53 nofun ⊢ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ No → Fun ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
54 funrel ⊢ Fun ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x → Rel ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
55 10 53 54 3syl ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → Rel ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
56 sssucid ⊢ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ⊆ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
57 relssres ⊢ Rel ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∧ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ⊆ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x → ι x ∈ B | ∀ y ∈ B ¬ y < s x ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x = ι x ∈ B | ∀ y ∈ B ¬ y < s x
58 55 56 57 sylancl ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ι x ∈ B | ∀ y ∈ B ¬ y < s x ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x = ι x ∈ B | ∀ y ∈ B ¬ y < s x
59 58 breq2d ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x < s ι x ∈ B | ∀ y ∈ B ¬ y < s x ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ↔ U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
60 2 13 sseldd ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → U ∈ No
61 nodmon ⊢ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ No → dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ On
62 10 61 syl ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ On
63 sucelon ⊢ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ On ↔ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ On
64 62 63 sylib ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ On
65 sltres ⊢ U ∈ No ∧ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ No ∧ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ On → U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x < s ι x ∈ B | ∀ y ∈ B ¬ y < s x ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x → U < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
66 60 10 64 65 syl3anc ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x < s ι x ∈ B | ∀ y ∈ B ¬ y < s x ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x → U < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
67 59 66 sylbird ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x < s ι x ∈ B | ∀ y ∈ B ¬ y < s x → U < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
68 52 67 mtod ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ¬ U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x < s ι x ∈ B | ∀ y ∈ B ¬ y < s x
69 1oex ⊢ 1 𝑜 ∈ V
70 69 prid1 ⊢ 1 𝑜 ∈ 1 𝑜 2 𝑜
71 70 noextend ⊢ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ No → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 ∈ No
72 10 71 syl ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 ∈ No
73 noreson ⊢ U ∈ No ∧ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ On → U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ No
74 60 64 73 syl2anc ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ No
75 sltso ⊢ < s Or No
76 sotr3 ⊢ < s Or No ∧ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 ∈ No ∧ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ No ∧ U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ No → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 < s ι x ∈ B | ∀ y ∈ B ¬ y < s x ∧ ¬ U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x < s ι x ∈ B | ∀ y ∈ B ¬ y < s x → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 < s U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
77 75 76 mpan ⊢ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 ∈ No ∧ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ No ∧ U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x ∈ No → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 < s ι x ∈ B | ∀ y ∈ B ¬ y < s x ∧ ¬ U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x < s ι x ∈ B | ∀ y ∈ B ¬ y < s x → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 < s U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
78 72 10 74 77 syl3anc ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 < s ι x ∈ B | ∀ y ∈ B ¬ y < s x ∧ ¬ U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x < s ι x ∈ B | ∀ y ∈ B ¬ y < s x → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 < s U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
79 12 68 78 mp2and ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 < s U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
80 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 𝑜
81 1 80 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 𝑜
82 81 adantr ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → T = ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜
83 81 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 𝑜
84 69 dmsnop ⊢ dom ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 = dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
85 84 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
86 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 𝑜
87 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
88 85 86 87 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
89 83 88 eqtrdi ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x → dom ⁡ T = suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
90 89 reseq2d ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x → U ↾ dom ⁡ T = U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
91 90 adantr ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → U ↾ dom ⁡ T = U ↾ suc ⁡ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
92 79 82 91 3brtr4d ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → T < s U ↾ dom ⁡ T
93 simpl ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x
94 simpr1 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → B ⊆ No
95 simpr2 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → B ∈ V
96 simpr3 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → U ∈ B
97 1 noinfbnd1lem6 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → T < s U ↾ dom ⁡ T
98 93 94 95 96 97 syl121anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → T < s U ↾ dom ⁡ T
99 92 98 pm2.61ian ⊢ B ⊆ No ∧ B ∈ V ∧ U ∈ B → T < s U ↾ dom ⁡ T