Metamath Proof Explorer


Theorem noinfbnd1lem1

Description: Lemma for noinfbnd1 . Establish a soft lower bound. (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 noinfbnd1lem1 ¬ x B y B ¬ y < s x B No B V U B ¬ U dom T < s 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 1 noinfno B No B V T No
3 2 3ad2ant2 ¬ x B y B ¬ y < s x B No B V U B T No
4 simp2l ¬ x B y B ¬ y < s x B No B V U B B No
5 simp3 ¬ x B y B ¬ y < s x B No B V U B U B
6 4 5 sseldd ¬ x B y B ¬ y < s x B No B V U B U No
7 nodmon T No dom T On
8 3 7 syl ¬ x B y B ¬ y < s x B No B V U B dom T On
9 noreson U No dom T On U dom T No
10 6 8 9 syl2anc ¬ x B y B ¬ y < s x B No B V U B U dom T No
11 ssidd ¬ x B y B ¬ y < s x B No B V U B dom T dom T
12 dmres dom U dom T = dom T dom U
13 inss1 dom T dom U dom T
14 12 13 eqsstri dom U dom T dom T
15 14 a1i ¬ x B y B ¬ y < s x B No B V U B dom U dom T dom T
16 nodmord T No Ord dom T
17 3 16 syl ¬ x B y B ¬ y < s x B No B V U B Ord dom T
18 ordsucss Ord dom T h dom T suc h dom T
19 17 18 syl ¬ x B y B ¬ y < s x B No B V U B h dom T suc h dom T
20 19 imp ¬ x B y B ¬ y < s x B No B V U B h dom T suc h dom T
21 20 resabs1d ¬ x B y B ¬ y < s x B No B V U B h dom T U dom T suc h = U suc h
22 1 noinfdm ¬ x B y B ¬ y < s x dom T = h | p B h dom p q B ¬ p < s q p suc h = q suc h
23 22 eleq2d ¬ x B y B ¬ y < s x h dom T h h | p B h dom p q B ¬ p < s q p suc h = q suc h
24 abid h h | p B h dom p q B ¬ p < s q p suc h = q suc h p B h dom p q B ¬ p < s q p suc h = q suc h
25 breq2 q = v p < s q p < s v
26 25 notbid q = v ¬ p < s q ¬ p < s v
27 reseq1 q = v q suc h = v suc h
28 27 eqeq2d q = v p suc h = q suc h p suc h = v suc h
29 26 28 imbi12d q = v ¬ p < s q p suc h = q suc h ¬ p < s v p suc h = v suc h
30 29 cbvralvw q B ¬ p < s q p suc h = q suc h v B ¬ p < s v p suc h = v suc h
31 30 anbi2i h dom p q B ¬ p < s q p suc h = q suc h h dom p v B ¬ p < s v p suc h = v suc h
32 31 rexbii p B h dom p q B ¬ p < s q p suc h = q suc h p B h dom p v B ¬ p < s v p suc h = v suc h
33 24 32 bitri h h | p B h dom p q B ¬ p < s q p suc h = q suc h p B h dom p v B ¬ p < s v p suc h = v suc h
34 23 33 bitrdi ¬ x B y B ¬ y < s x h dom T p B h dom p v B ¬ p < s v p suc h = v suc h
35 34 3ad2ant1 ¬ x B y B ¬ y < s x B No B V U B h dom T p B h dom p v B ¬ p < s v p suc h = v suc h
36 simpl2l ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h B No
37 simprl ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h p B
38 36 37 sseldd ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h p No
39 6 adantr ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h U No
40 sltso < s Or No
41 soasym < s Or No p No U No p < s U ¬ U < s p
42 40 41 mpan p No U No p < s U ¬ U < s p
43 38 39 42 syl2anc ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h p < s U ¬ U < s p
44 nodmon p No dom p On
45 38 44 syl ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h dom p On
46 simprrl ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h h dom p
47 onelon dom p On h dom p h On
48 45 46 47 syl2anc ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h h On
49 sucelon h On suc h On
50 48 49 sylib ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h suc h On
51 sltres U No p No suc h On U suc h < s p suc h U < s p
52 39 38 50 51 syl3anc ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h U suc h < s p suc h U < s p
53 43 52 nsyld ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h p < s U ¬ U suc h < s p suc h
54 noreson U No suc h On U suc h No
55 39 50 54 syl2anc ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h U suc h No
56 sonr < s Or No U suc h No ¬ U suc h < s U suc h
57 40 56 mpan U suc h No ¬ U suc h < s U suc h
58 55 57 syl ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h ¬ U suc h < s U suc h
59 58 adantr ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h ¬ p < s U ¬ U suc h < s U suc h
60 breq2 v = U p < s v p < s U
61 60 notbid v = U ¬ p < s v ¬ p < s U
62 reseq1 v = U v suc h = U suc h
63 62 eqeq2d v = U p suc h = v suc h p suc h = U suc h
64 61 63 imbi12d v = U ¬ p < s v p suc h = v suc h ¬ p < s U p suc h = U suc h
65 simprrr ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h v B ¬ p < s v p suc h = v suc h
66 simpl3 ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h U B
67 64 65 66 rspcdva ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h ¬ p < s U p suc h = U suc h
68 67 imp ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h ¬ p < s U p suc h = U suc h
69 68 breq2d ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h ¬ p < s U U suc h < s p suc h U suc h < s U suc h
70 59 69 mtbird ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h ¬ p < s U ¬ U suc h < s p suc h
71 70 ex ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h ¬ p < s U ¬ U suc h < s p suc h
72 53 71 pm2.61d ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h ¬ U suc h < s p suc h
73 simpl1 ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h ¬ x B y B ¬ y < s x
74 simpl2 ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h B No B V
75 1 noinfres ¬ x B y B ¬ y < s x B No B V p B h dom p v B ¬ p < s v p suc h = v suc h T suc h = p suc h
76 73 74 37 46 65 75 syl113anc ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h T suc h = p suc h
77 76 breq2d ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h U suc h < s T suc h U suc h < s p suc h
78 72 77 mtbird ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h ¬ U suc h < s T suc h
79 78 rexlimdvaa ¬ x B y B ¬ y < s x B No B V U B p B h dom p v B ¬ p < s v p suc h = v suc h ¬ U suc h < s T suc h
80 35 79 sylbid ¬ x B y B ¬ y < s x B No B V U B h dom T ¬ U suc h < s T suc h
81 80 imp ¬ x B y B ¬ y < s x B No B V U B h dom T ¬ U suc h < s T suc h
82 21 81 eqnbrtrd ¬ x B y B ¬ y < s x B No B V U B h dom T ¬ U dom T suc h < s T suc h
83 82 ralrimiva ¬ x B y B ¬ y < s x B No B V U B h dom T ¬ U dom T suc h < s T suc h
84 noresle T No U dom T No dom T dom T dom U dom T dom T h dom T ¬ U dom T suc h < s T suc h ¬ U dom T < s T
85 3 10 11 15 83 84 syl23anc ¬ x B y B ¬ y < s x B No B V U B ¬ U dom T < s T