Metamath Proof Explorer


Theorem noinfbnd1lem5

Description: Lemma for noinfbnd1 . If U is a prolongment of T and in B , then ( Udom T ) is not 2o . (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 noinfbnd1lem5 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T 2 𝑜

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 1 noinfno B No B V T No
3 2 3ad2ant2 ¬ x B y B ¬ y < s x B No B V U B U dom T = T T No
4 3 adantl z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T T No
5 nodmord T No Ord dom T
6 4 5 syl z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T Ord dom T
7 ordirr Ord dom T ¬ dom T dom T
8 6 7 syl z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T ¬ dom T dom T
9 simpr3l z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U B
10 9 adantr z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 U B
11 ndmfv ¬ dom T dom U U dom T =
12 2on0 2 𝑜
13 12 necomi 2 𝑜
14 neeq1 U dom T = U dom T 2 𝑜 2 𝑜
15 13 14 mpbiri U dom T = U dom T 2 𝑜
16 11 15 syl ¬ dom T dom U U dom T 2 𝑜
17 16 neneqd ¬ dom T dom U ¬ U dom T = 2 𝑜
18 17 con4i U dom T = 2 𝑜 dom T dom U
19 18 adantl z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 dom T dom U
20 simpl2l ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 B No
21 20 adantr ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 B No
22 simpl3l ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 U B
23 22 adantr ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 U B
24 21 23 sseldd ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 U No
25 nofun U No Fun U
26 24 25 syl ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 Fun U
27 simprll ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 z B
28 21 27 sseldd ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 z No
29 nofun z No Fun z
30 28 29 syl ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 Fun z
31 simpl3r ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 U dom T = T
32 31 adantr ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 U dom T = T
33 simpll1 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x
34 simpll2 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 B No B V
35 simpll3 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 U B U dom T = T
36 simprl ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 z B ¬ U < s z
37 1 noinfbnd1lem2 ¬ x B y B ¬ y < s x B No B V U B U dom T = T z B ¬ U < s z z dom T = T
38 33 34 35 36 37 syl112anc ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 z dom T = T
39 32 38 eqtr4d ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 U dom T = z dom T
40 simplr ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 U dom T = 2 𝑜
41 40 18 syl ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 dom T dom U
42 simprr ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 z dom T = 2 𝑜
43 ndmfv ¬ dom T dom z z dom T =
44 neeq1 z dom T = z dom T 2 𝑜 2 𝑜
45 13 44 mpbiri z dom T = z dom T 2 𝑜
46 43 45 syl ¬ dom T dom z z dom T 2 𝑜
47 46 neneqd ¬ dom T dom z ¬ z dom T = 2 𝑜
48 47 con4i z dom T = 2 𝑜 dom T dom z
49 42 48 syl ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 dom T dom z
50 40 42 eqtr4d ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 U dom T = z dom T
51 eqfunressuc Fun U Fun z U dom T = z dom T dom T dom U dom T dom z U dom T = z dom T U suc dom T = z suc dom T
52 26 30 39 41 49 50 51 syl213anc ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 U suc dom T = z suc dom T
53 52 expr ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 U suc dom T = z suc dom T
54 53 expr ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 U suc dom T = z suc dom T
55 54 a2d ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 ¬ U < s z U suc dom T = z suc dom T
56 55 ralimdva ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z z dom T = 2 𝑜 z B ¬ U < s z U suc dom T = z suc dom T
57 56 impcom z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z U suc dom T = z suc dom T
58 57 anassrs z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 z B ¬ U < s z U suc dom T = z suc dom T
59 dmeq p = U dom p = dom U
60 59 eleq2d p = U dom T dom p dom T dom U
61 breq1 p = U p < s z U < s z
62 61 notbid p = U ¬ p < s z ¬ U < s z
63 reseq1 p = U p suc dom T = U suc dom T
64 63 eqeq1d p = U p suc dom T = z suc dom T U suc dom T = z suc dom T
65 62 64 imbi12d p = U ¬ p < s z p suc dom T = z suc dom T ¬ U < s z U suc dom T = z suc dom T
66 65 ralbidv p = U z B ¬ p < s z p suc dom T = z suc dom T z B ¬ U < s z U suc dom T = z suc dom T
67 60 66 anbi12d p = U dom T dom p z B ¬ p < s z p suc dom T = z suc dom T dom T dom U z B ¬ U < s z U suc dom T = z suc dom T
68 67 rspcev U B dom T dom U z B ¬ U < s z U suc dom T = z suc dom T p B dom T dom p z B ¬ p < s z p suc dom T = z suc dom T
69 10 19 58 68 syl12anc z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 p B dom T dom p z B ¬ p < s z p suc dom T = z suc dom T
70 nodmon T No dom T On
71 4 70 syl z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T dom T On
72 71 adantr z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 dom T On
73 eleq1 a = dom T a dom p dom T dom p
74 suceq a = dom T suc a = suc dom T
75 74 reseq2d a = dom T p suc a = p suc dom T
76 74 reseq2d a = dom T z suc a = z suc dom T
77 75 76 eqeq12d a = dom T p suc a = z suc a p suc dom T = z suc dom T
78 77 imbi2d a = dom T ¬ p < s z p suc a = z suc a ¬ p < s z p suc dom T = z suc dom T
79 78 ralbidv a = dom T z B ¬ p < s z p suc a = z suc a z B ¬ p < s z p suc dom T = z suc dom T
80 73 79 anbi12d a = dom T a dom p z B ¬ p < s z p suc a = z suc a dom T dom p z B ¬ p < s z p suc dom T = z suc dom T
81 80 rexbidv a = dom T p B a dom p z B ¬ p < s z p suc a = z suc a p B dom T dom p z B ¬ p < s z p suc dom T = z suc dom T
82 81 elabg dom T On dom T a | p B a dom p z B ¬ p < s z p suc a = z suc a p B dom T dom p z B ¬ p < s z p suc dom T = z suc dom T
83 72 82 syl z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 dom T a | p B a dom p z B ¬ p < s z p suc a = z suc a p B dom T dom p z B ¬ p < s z p suc dom T = z suc dom T
84 69 83 mpbird z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 dom T a | p B a dom p z B ¬ p < s z p suc a = z suc a
85 1 noinfdm ¬ x B y B ¬ y < s x dom T = a | p B a dom p z B ¬ p < s z p suc a = z suc a
86 85 3ad2ant1 ¬ x B y B ¬ y < s x B No B V U B U dom T = T dom T = a | p B a dom p z B ¬ p < s z p suc a = z suc a
87 86 adantl z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T dom T = a | p B a dom p z B ¬ p < s z p suc a = z suc a
88 87 adantr z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 dom T = a | p B a dom p z B ¬ p < s z p suc a = z suc a
89 88 eleq2d z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 dom T dom T dom T a | p B a dom p z B ¬ p < s z p suc a = z suc a
90 84 89 mpbird z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T = 2 𝑜 dom T dom T
91 8 90 mtand z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T ¬ U dom T = 2 𝑜
92 91 neqned z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T 2 𝑜
93 rexanali z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ z B ¬ U < s z z dom T = 2 𝑜
94 simpr1 z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T ¬ x B y B ¬ y < s x
95 simpr2 z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T B No B V
96 simplll z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T z B
97 simpr3 z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U B U dom T = T
98 simpll z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T z B ¬ U < s z
99 94 95 97 98 37 syl112anc z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T z dom T = T
100 1 noinfbnd1lem4 ¬ x B y B ¬ y < s x B No B V z B z dom T = T z dom T
101 94 95 96 99 100 syl112anc z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T z dom T
102 101 neneqd z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T ¬ z dom T =
103 102 pm2.21d z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T z dom T = U dom T 2 𝑜
104 1 noinfbnd1lem3 ¬ x B y B ¬ y < s x B No B V z B z dom T = T z dom T 1 𝑜
105 94 95 96 99 104 syl112anc z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T z dom T 1 𝑜
106 105 neneqd z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T ¬ z dom T = 1 𝑜
107 106 pm2.21d z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T z dom T = 1 𝑜 U dom T 2 𝑜
108 simplr z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T ¬ z dom T = 2 𝑜
109 simpr2l z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T B No
110 109 96 sseldd z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T z No
111 nofv z No z dom T = z dom T = 1 𝑜 z dom T = 2 𝑜
112 110 111 syl z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T z dom T = z dom T = 1 𝑜 z dom T = 2 𝑜
113 3orel3 ¬ z dom T = 2 𝑜 z dom T = z dom T = 1 𝑜 z dom T = 2 𝑜 z dom T = z dom T = 1 𝑜
114 108 112 113 sylc z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T z dom T = z dom T = 1 𝑜
115 103 107 114 mpjaod z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T 2 𝑜
116 115 ex z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T 2 𝑜
117 116 anasss z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T 2 𝑜
118 117 rexlimiva z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T 2 𝑜
119 118 imp z B ¬ U < s z ¬ z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T 2 𝑜
120 93 119 sylanbr ¬ z B ¬ U < s z z dom T = 2 𝑜 ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T 2 𝑜
121 92 120 pm2.61ian ¬ x B y B ¬ y < s x B No B V U B U dom T = T U dom T 2 𝑜