Metamath Proof Explorer

Theorem noinfbnd2

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

Ref Expression
Hypothesis noinfbnd2.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 noinfbnd2 ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No → ∀ b ∈ B Z < s b ↔ ¬ T < s Z ↾ dom ⁡ T

Proof

Step Hyp Ref Expression
1 noinfbnd2.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 nfv ⊢ Ⅎ x B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b
3 nfre1 ⊢ Ⅎ x ∃ x ∈ B ∀ y ∈ B ¬ y < s x
4 nfriota1 ⊢ Ⅎ _ x ι x ∈ B | ∀ y ∈ B ¬ y < s x
5 4 nfdm ⊢ Ⅎ _ x dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x
6 nfcv ⊢ Ⅎ _ x 1 𝑜
7 5 6 nfop ⊢ Ⅎ _ x dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜
8 7 nfsn ⊢ Ⅎ _ x dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜
9 4 8 nfun ⊢ Ⅎ _ x ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜
10 nfcv ⊢ Ⅎ _ x y | ∃ u ∈ B y ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ y = v ↾ suc ⁡ y
11 nfiota1 ⊢ Ⅎ _ x ι x | ∃ u ∈ B g ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x
12 10 11 nfmpt ⊢ Ⅎ _ x 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
13 3 9 12 nfif ⊢ Ⅎ _ 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
14 1 13 nfcxfr ⊢ Ⅎ _ x T
15 nfcv ⊢ Ⅎ _ x < s
16 nfcv ⊢ Ⅎ _ x Z
17 14 nfdm ⊢ Ⅎ _ x dom ⁡ T
18 16 17 nfres ⊢ Ⅎ _ x Z ↾ dom ⁡ T
19 14 15 18 nfbr ⊢ Ⅎ x T < s Z ↾ dom ⁡ T
20 19 nfn ⊢ Ⅎ x ¬ T < s Z ↾ dom ⁡ T
21 2 20 nfim ⊢ Ⅎ x B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ¬ T < s Z ↾ dom ⁡ T
22 noinfbnd2lem1 ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ¬ x ∪ dom ⁡ x 1 𝑜 < s Z ↾ suc ⁡ dom ⁡ x
23 22 3expb ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ¬ x ∪ dom ⁡ x 1 𝑜 < s Z ↾ suc ⁡ dom ⁡ 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 ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ∃ x ∈ B ∀ y ∈ B ¬ y < s x
26 25 iftrued ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → 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 𝑜
27 simpl ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → x ∈ B ∧ ∀ y ∈ B ¬ y < s x
28 simprl1 ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → B ⊆ No
29 nominmo ⊢ B ⊆ No → ∃* x ∈ B ∀ y ∈ B ¬ y < s x
30 28 29 syl ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ∃* x ∈ B ∀ y ∈ B ¬ y < s x
31 reu5 ⊢ ∃! x ∈ B ∀ y ∈ B ¬ y < s x ↔ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ ∃* x ∈ B ∀ y ∈ B ¬ y < s x
32 25 30 31 sylanbrc ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ∃! x ∈ B ∀ y ∈ B ¬ y < s x
33 riota1 ⊢ ∃! x ∈ B ∀ y ∈ B ¬ y < s x → x ∈ B ∧ ∀ y ∈ B ¬ y < s x ↔ ι x ∈ B | ∀ y ∈ B ¬ y < s x = x
34 32 33 syl ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → x ∈ B ∧ ∀ y ∈ B ¬ y < s x ↔ ι x ∈ B | ∀ y ∈ B ¬ y < s x = x
35 27 34 mpbid ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ι x ∈ B | ∀ y ∈ B ¬ y < s x = x
36 35 dmeqd ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x = dom ⁡ x
37 36 opeq1d ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 = dom ⁡ x 1 𝑜
38 37 sneqd ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 = dom ⁡ x 1 𝑜
39 35 38 uneq12d ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 = x ∪ dom ⁡ x 1 𝑜
40 26 39 eqtrd ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → 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 ∪ dom ⁡ x 1 𝑜
41 1 40 eqtrid ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → T = x ∪ dom ⁡ x 1 𝑜
42 41 dmeqd ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → dom ⁡ T = dom ⁡ x ∪ dom ⁡ x 1 𝑜
43 1oex ⊢ 1 𝑜 ∈ V
44 43 dmsnop ⊢ dom ⁡ dom ⁡ x 1 𝑜 = dom ⁡ x
45 44 uneq2i ⊢ dom ⁡ x ∪ dom ⁡ dom ⁡ x 1 𝑜 = dom ⁡ x ∪ dom ⁡ x
46 dmun ⊢ dom ⁡ x ∪ dom ⁡ x 1 𝑜 = dom ⁡ x ∪ dom ⁡ dom ⁡ x 1 𝑜
47 df-suc ⊢ suc ⁡ dom ⁡ x = dom ⁡ x ∪ dom ⁡ x
48 45 46 47 3eqtr4ri ⊢ suc ⁡ dom ⁡ x = dom ⁡ x ∪ dom ⁡ x 1 𝑜
49 42 48 eqtr4di ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → dom ⁡ T = suc ⁡ dom ⁡ x
50 49 reseq2d ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → Z ↾ dom ⁡ T = Z ↾ suc ⁡ dom ⁡ x
51 41 50 breq12d ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → T < s Z ↾ dom ⁡ T ↔ x ∪ dom ⁡ x 1 𝑜 < s Z ↾ suc ⁡ dom ⁡ x
52 23 51 mtbird ⊢ x ∈ B ∧ ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ¬ T < s Z ↾ dom ⁡ T
53 52 exp31 ⊢ x ∈ B → ∀ y ∈ B ¬ y < s x → B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ¬ T < s Z ↾ dom ⁡ T
54 21 53 rexlimi ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x → B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ¬ T < s Z ↾ dom ⁡ T
55 54 imp ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ¬ T < s Z ↾ dom ⁡ T
56 simprl3 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → Z ∈ No
57 1 noinfno ⊢ B ⊆ No ∧ B ∈ V → T ∈ No
58 57 3adant3 ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No → T ∈ No
59 58 ad2antrl ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → T ∈ No
60 nodmon ⊢ T ∈ No → dom ⁡ T ∈ On
61 59 60 syl ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → dom ⁡ T ∈ On
62 noreson ⊢ Z ∈ No ∧ dom ⁡ T ∈ On → Z ↾ dom ⁡ T ∈ No
63 56 61 62 syl2anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → Z ↾ dom ⁡ T ∈ No
64 nofun ⊢ T ∈ No → Fun ⁡ T
65 funrel ⊢ Fun ⁡ T → Rel ⁡ T
66 58 64 65 3syl ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No → Rel ⁡ T
67 66 ad2antrl ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → Rel ⁡ T
68 resdm ⊢ Rel ⁡ T → T ↾ dom ⁡ T = T
69 67 68 syl ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → T ↾ dom ⁡ T = T
70 69 59 eqeltrd ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → T ↾ dom ⁡ T ∈ No
71 resdmss ⊢ dom ⁡ Z ↾ dom ⁡ T ⊆ dom ⁡ T
72 71 a1i ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → dom ⁡ Z ↾ dom ⁡ T ⊆ dom ⁡ T
73 resdmss ⊢ dom ⁡ T ↾ dom ⁡ T ⊆ dom ⁡ T
74 73 a1i ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → dom ⁡ T ↾ dom ⁡ T ⊆ dom ⁡ T
75 1 noinfdm ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x → dom ⁡ T = g | ∃ p ∈ B g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g
76 75 eqabrd ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x → g ∈ dom ⁡ T ↔ ∃ p ∈ B g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g
77 76 adantr ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → g ∈ dom ⁡ T ↔ ∃ p ∈ B g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g
78 simpll ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x
79 simprl1 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → B ⊆ No
80 79 adantr ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → B ⊆ No
81 simprl2 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → B ∈ V
82 81 adantr ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → B ∈ V
83 simprl ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → p ∈ B
84 simprrl ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → g ∈ dom ⁡ p
85 simprrr ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g
86 breq2 ⊢ q = v → p < s q ↔ p < s v
87 86 notbid ⊢ q = v → ¬ p < s q ↔ ¬ p < s v
88 reseq1 ⊢ q = v → q ↾ suc ⁡ g = v ↾ suc ⁡ g
89 88 eqeq2d ⊢ q = v → p ↾ suc ⁡ g = q ↾ suc ⁡ g ↔ p ↾ suc ⁡ g = v ↾ suc ⁡ g
90 87 89 imbi12d ⊢ q = v → ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g ↔ ¬ p < s v → p ↾ suc ⁡ g = v ↾ suc ⁡ g
91 90 cbvralvw ⊢ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g ↔ ∀ v ∈ B ¬ p < s v → p ↾ suc ⁡ g = v ↾ suc ⁡ g
92 85 91 sylib ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → ∀ v ∈ B ¬ p < s v → p ↾ suc ⁡ g = v ↾ suc ⁡ g
93 1 noinfres ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ v ∈ B ¬ p < s v → p ↾ suc ⁡ g = v ↾ suc ⁡ g → T ↾ suc ⁡ g = p ↾ suc ⁡ g
94 78 80 82 83 84 92 93 syl123anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → T ↾ suc ⁡ g = p ↾ suc ⁡ g
95 breq2 ⊢ b = p → Z < s b ↔ Z < s p
96 simplrr ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → ∀ b ∈ B Z < s b
97 95 96 83 rspcdva ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → Z < s p
98 56 adantr ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → Z ∈ No
99 80 83 sseldd ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → p ∈ No
100 ltsso ⊢ < s Or No
101 soasym ⊢ < s Or No ∧ Z ∈ No ∧ p ∈ No → Z < s p → ¬ p < s Z
102 100 101 mpan ⊢ Z ∈ No ∧ p ∈ No → Z < s p → ¬ p < s Z
103 98 99 102 syl2anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → Z < s p → ¬ p < s Z
104 97 103 mpd ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → ¬ p < s Z
105 nodmon ⊢ p ∈ No → dom ⁡ p ∈ On
106 99 105 syl ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → dom ⁡ p ∈ On
107 onelon ⊢ dom ⁡ p ∈ On ∧ g ∈ dom ⁡ p → g ∈ On
108 106 84 107 syl2anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → g ∈ On
109 onsucb ⊢ g ∈ On ↔ suc ⁡ g ∈ On
110 108 109 sylib ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → suc ⁡ g ∈ On
111 ltsres ⊢ p ∈ No ∧ Z ∈ No ∧ suc ⁡ g ∈ On → p ↾ suc ⁡ g < s Z ↾ suc ⁡ g → p < s Z
112 99 98 110 111 syl3anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → p ↾ suc ⁡ g < s Z ↾ suc ⁡ g → p < s Z
113 104 112 mtod ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → ¬ p ↾ suc ⁡ g < s Z ↾ suc ⁡ g
114 94 113 eqnbrtrd ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ p ∈ B ∧ g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → ¬ T ↾ suc ⁡ g < s Z ↾ suc ⁡ g
115 114 rexlimdvaa ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ∃ p ∈ B g ∈ dom ⁡ p ∧ ∀ q ∈ B ¬ p < s q → p ↾ suc ⁡ g = q ↾ suc ⁡ g → ¬ T ↾ suc ⁡ g < s Z ↾ suc ⁡ g
116 77 115 sylbid ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → g ∈ dom ⁡ T → ¬ T ↾ suc ⁡ g < s Z ↾ suc ⁡ g
117 116 imp ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ g ∈ dom ⁡ T → ¬ T ↾ suc ⁡ g < s Z ↾ suc ⁡ g
118 nodmord ⊢ T ∈ No → Ord ⁡ dom ⁡ T
119 ordsucss ⊢ Ord ⁡ dom ⁡ T → g ∈ dom ⁡ T → suc ⁡ g ⊆ dom ⁡ T
120 59 118 119 3syl ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → g ∈ dom ⁡ T → suc ⁡ g ⊆ dom ⁡ T
121 120 imp ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ g ∈ dom ⁡ T → suc ⁡ g ⊆ dom ⁡ T
122 121 resabs1d ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ g ∈ dom ⁡ T → T ↾ dom ⁡ T ↾ suc ⁡ g = T ↾ suc ⁡ g
123 121 resabs1d ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ g ∈ dom ⁡ T → Z ↾ dom ⁡ T ↾ suc ⁡ g = Z ↾ suc ⁡ g
124 122 123 breq12d ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ g ∈ dom ⁡ T → T ↾ dom ⁡ T ↾ suc ⁡ g < s Z ↾ dom ⁡ T ↾ suc ⁡ g ↔ T ↾ suc ⁡ g < s Z ↾ suc ⁡ g
125 117 124 mtbird ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b ∧ g ∈ dom ⁡ T → ¬ T ↾ dom ⁡ T ↾ suc ⁡ g < s Z ↾ dom ⁡ T ↾ suc ⁡ g
126 125 ralrimiva ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ∀ g ∈ dom ⁡ T ¬ T ↾ dom ⁡ T ↾ suc ⁡ g < s Z ↾ dom ⁡ T ↾ suc ⁡ g
127 noresle ⊢ Z ↾ dom ⁡ T ∈ No ∧ T ↾ dom ⁡ T ∈ No ∧ dom ⁡ Z ↾ dom ⁡ T ⊆ dom ⁡ T ∧ dom ⁡ T ↾ dom ⁡ T ⊆ dom ⁡ T ∧ ∀ g ∈ dom ⁡ T ¬ T ↾ dom ⁡ T ↾ suc ⁡ g < s Z ↾ dom ⁡ T ↾ suc ⁡ g → ¬ T ↾ dom ⁡ T < s Z ↾ dom ⁡ T
128 63 70 72 74 126 127 syl23anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ¬ T ↾ dom ⁡ T < s Z ↾ dom ⁡ T
129 69 breq1d ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → T ↾ dom ⁡ T < s Z ↾ dom ⁡ T ↔ T < s Z ↾ dom ⁡ T
130 128 129 mtbid ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ¬ T < s Z ↾ dom ⁡ T
131 55 130 pm2.61ian ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ∀ b ∈ B Z < s b → ¬ T < s Z ↾ dom ⁡ T
132 simplr ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → ¬ T < s Z ↾ dom ⁡ T
133 simpll1 ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → B ⊆ No
134 simpll2 ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → B ∈ V
135 simpr ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → b ∈ B
136 1 noinfbnd1 ⊢ B ⊆ No ∧ B ∈ V ∧ b ∈ B → T < s b ↾ dom ⁡ T
137 133 134 135 136 syl3anc ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → T < s b ↾ dom ⁡ T
138 simpl3 ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T → Z ∈ No
139 simpl1 ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T → B ⊆ No
140 simpl2 ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T → B ∈ V
141 139 140 57 syl2anc ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T → T ∈ No
142 141 60 syl ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T → dom ⁡ T ∈ On
143 138 142 62 syl2anc ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T → Z ↾ dom ⁡ T ∈ No
144 143 adantr ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → Z ↾ dom ⁡ T ∈ No
145 141 adantr ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → T ∈ No
146 139 sselda ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → b ∈ No
147 142 adantr ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → dom ⁡ T ∈ On
148 noreson ⊢ b ∈ No ∧ dom ⁡ T ∈ On → b ↾ dom ⁡ T ∈ No
149 146 147 148 syl2anc ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → b ↾ dom ⁡ T ∈ No
150 sotr2 ⊢ < s Or No ∧ Z ↾ dom ⁡ T ∈ No ∧ T ∈ No ∧ b ↾ dom ⁡ T ∈ No → ¬ T < s Z ↾ dom ⁡ T ∧ T < s b ↾ dom ⁡ T → Z ↾ dom ⁡ T < s b ↾ dom ⁡ T
151 100 150 mpan ⊢ Z ↾ dom ⁡ T ∈ No ∧ T ∈ No ∧ b ↾ dom ⁡ T ∈ No → ¬ T < s Z ↾ dom ⁡ T ∧ T < s b ↾ dom ⁡ T → Z ↾ dom ⁡ T < s b ↾ dom ⁡ T
152 144 145 149 151 syl3anc ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → ¬ T < s Z ↾ dom ⁡ T ∧ T < s b ↾ dom ⁡ T → Z ↾ dom ⁡ T < s b ↾ dom ⁡ T
153 132 137 152 mp2and ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → Z ↾ dom ⁡ T < s b ↾ dom ⁡ T
154 simpll3 ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → Z ∈ No
155 ltsres ⊢ Z ∈ No ∧ b ∈ No ∧ dom ⁡ T ∈ On → Z ↾ dom ⁡ T < s b ↾ dom ⁡ T → Z < s b
156 154 146 147 155 syl3anc ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → Z ↾ dom ⁡ T < s b ↾ dom ⁡ T → Z < s b
157 153 156 mpd ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T ∧ b ∈ B → Z < s b
158 157 ralrimiva ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No ∧ ¬ T < s Z ↾ dom ⁡ T → ∀ b ∈ B Z < s b
159 131 158 impbida ⊢ B ⊆ No ∧ B ∈ V ∧ Z ∈ No → ∀ b ∈ B Z < s b ↔ ¬ T < s Z ↾ dom ⁡ T