Metamath Proof Explorer


Theorem nosupbnd1lem1

Description: Lemma for nosupbnd1 . Establish a soft upper bound. (Contributed by Scott Fenton, 5-Dec-2021)

Ref Expression
Hypothesis nosupbnd1.1 S = if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
Assertion nosupbnd1lem1 ¬ x A y A ¬ x < s y A No A V U A ¬ S < s U dom S

Proof

Step Hyp Ref Expression
1 nosupbnd1.1 S = if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
2 simp2l ¬ x A y A ¬ x < s y A No A V U A A No
3 simp3 ¬ x A y A ¬ x < s y A No A V U A U A
4 2 3 sseldd ¬ x A y A ¬ x < s y A No A V U A U No
5 1 nosupno A No A V S No
6 5 3ad2ant2 ¬ x A y A ¬ x < s y A No A V U A S No
7 nodmon S No dom S On
8 6 7 syl ¬ x A y A ¬ x < s y A No A V U A dom S On
9 noreson U No dom S On U dom S No
10 4 8 9 syl2anc ¬ x A y A ¬ x < s y A No A V U A U dom S No
11 dmres dom U dom S = dom S dom U
12 inss1 dom S dom U dom S
13 11 12 eqsstri dom U dom S dom S
14 13 a1i ¬ x A y A ¬ x < s y A No A V U A dom U dom S dom S
15 ssidd ¬ x A y A ¬ x < s y A No A V U A dom S dom S
16 iffalse ¬ x A y A ¬ x < s y if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x = g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
17 1 16 syl5eq ¬ x A y A ¬ x < s y S = g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
18 17 dmeqd ¬ x A y A ¬ x < s y dom S = dom g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
19 iotaex ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x V
20 eqid g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x = g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
21 19 20 dmmpti dom g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x = y | u A y dom u v A ¬ v < s u u suc y = v suc y
22 18 21 eqtrdi ¬ x A y A ¬ x < s y dom S = y | u A y dom u v A ¬ v < s u u suc y = v suc y
23 22 eleq2d ¬ x A y A ¬ x < s y h dom S h y | u A y dom u v A ¬ v < s u u suc y = v suc y
24 vex h V
25 eleq1w y = h y dom u h dom u
26 suceq y = h suc y = suc h
27 26 reseq2d y = h u suc y = u suc h
28 26 reseq2d y = h v suc y = v suc h
29 27 28 eqeq12d y = h u suc y = v suc y u suc h = v suc h
30 29 imbi2d y = h ¬ v < s u u suc y = v suc y ¬ v < s u u suc h = v suc h
31 30 ralbidv y = h v A ¬ v < s u u suc y = v suc y v A ¬ v < s u u suc h = v suc h
32 25 31 anbi12d y = h y dom u v A ¬ v < s u u suc y = v suc y h dom u v A ¬ v < s u u suc h = v suc h
33 32 rexbidv y = h u A y dom u v A ¬ v < s u u suc y = v suc y u A h dom u v A ¬ v < s u u suc h = v suc h
34 dmeq u = p dom u = dom p
35 34 eleq2d u = p h dom u h dom p
36 breq2 u = p v < s u v < s p
37 36 notbid u = p ¬ v < s u ¬ v < s p
38 reseq1 u = p u suc h = p suc h
39 38 eqeq1d u = p u suc h = v suc h p suc h = v suc h
40 37 39 imbi12d u = p ¬ v < s u u suc h = v suc h ¬ v < s p p suc h = v suc h
41 40 ralbidv u = p v A ¬ v < s u u suc h = v suc h v A ¬ v < s p p suc h = v suc h
42 35 41 anbi12d u = p h dom u v A ¬ v < s u u suc h = v suc h h dom p v A ¬ v < s p p suc h = v suc h
43 42 cbvrexvw u A h dom u v A ¬ v < s u u suc h = v suc h p A h dom p v A ¬ v < s p p suc h = v suc h
44 33 43 bitrdi y = h u A y dom u v A ¬ v < s u u suc y = v suc y p A h dom p v A ¬ v < s p p suc h = v suc h
45 24 44 elab h y | u A y dom u v A ¬ v < s u u suc y = v suc y p A h dom p v A ¬ v < s p p suc h = v suc h
46 23 45 bitrdi ¬ x A y A ¬ x < s y h dom S p A h dom p v A ¬ v < s p p suc h = v suc h
47 46 3ad2ant1 ¬ x A y A ¬ x < s y A No A V U A h dom S p A h dom p v A ¬ v < s p p suc h = v suc h
48 simpl1 ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h ¬ x A y A ¬ x < s y
49 simpl2 ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h A No A V
50 simprl ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h p A
51 simprrl ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h h dom p
52 simprrr ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h v A ¬ v < s p p suc h = v suc h
53 1 nosupres ¬ x A y A ¬ x < s y A No A V p A h dom p v A ¬ v < s p p suc h = v suc h S suc h = p suc h
54 48 49 50 51 52 53 syl113anc ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h S suc h = p suc h
55 simpl2l ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h A No
56 55 50 sseldd ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h p No
57 4 adantr ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h U No
58 sltso < s Or No
59 soasym < s Or No p No U No p < s U ¬ U < s p
60 58 59 mpan p No U No p < s U ¬ U < s p
61 56 57 60 syl2anc ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h p < s U ¬ U < s p
62 simpl3 ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h U A
63 breq1 v = U v < s p U < s p
64 63 notbid v = U ¬ v < s p ¬ U < s p
65 reseq1 v = U v suc h = U suc h
66 65 eqeq2d v = U p suc h = v suc h p suc h = U suc h
67 64 66 imbi12d v = U ¬ v < s p p suc h = v suc h ¬ U < s p p suc h = U suc h
68 67 rspcv U A v A ¬ v < s p p suc h = v suc h ¬ U < s p p suc h = U suc h
69 62 52 68 sylc ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h ¬ U < s p p suc h = U suc h
70 61 69 syld ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h p < s U p suc h = U suc h
71 70 imp ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h p < s U p suc h = U suc h
72 nodmon p No dom p On
73 56 72 syl ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h dom p On
74 onelon dom p On h dom p h On
75 73 51 74 syl2anc ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h h On
76 sucelon h On suc h On
77 75 76 sylib ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h suc h On
78 noreson U No suc h On U suc h No
79 57 77 78 syl2anc ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h U suc h No
80 sonr < s Or No U suc h No ¬ U suc h < s U suc h
81 58 80 mpan U suc h No ¬ U suc h < s U suc h
82 79 81 syl ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h ¬ U suc h < s U suc h
83 82 adantr ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h p < s U ¬ U suc h < s U suc h
84 71 83 eqnbrtrd ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h p < s U ¬ p suc h < s U suc h
85 84 ex ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h p < s U ¬ p suc h < s U suc h
86 sltres p No U No suc h On p suc h < s U suc h p < s U
87 56 57 77 86 syl3anc ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h p suc h < s U suc h p < s U
88 87 con3d ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h ¬ p < s U ¬ p suc h < s U suc h
89 85 88 pm2.61d ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h ¬ p suc h < s U suc h
90 54 89 eqnbrtrd ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h ¬ S suc h < s U suc h
91 90 rexlimdvaa ¬ x A y A ¬ x < s y A No A V U A p A h dom p v A ¬ v < s p p suc h = v suc h ¬ S suc h < s U suc h
92 47 91 sylbid ¬ x A y A ¬ x < s y A No A V U A h dom S ¬ S suc h < s U suc h
93 92 imp ¬ x A y A ¬ x < s y A No A V U A h dom S ¬ S suc h < s U suc h
94 nodmord S No Ord dom S
95 ordsucss Ord dom S h dom S suc h dom S
96 6 94 95 3syl ¬ x A y A ¬ x < s y A No A V U A h dom S suc h dom S
97 96 imp ¬ x A y A ¬ x < s y A No A V U A h dom S suc h dom S
98 97 resabs1d ¬ x A y A ¬ x < s y A No A V U A h dom S U dom S suc h = U suc h
99 98 breq2d ¬ x A y A ¬ x < s y A No A V U A h dom S S suc h < s U dom S suc h S suc h < s U suc h
100 93 99 mtbird ¬ x A y A ¬ x < s y A No A V U A h dom S ¬ S suc h < s U dom S suc h
101 100 ralrimiva ¬ x A y A ¬ x < s y A No A V U A h dom S ¬ S suc h < s U dom S suc h
102 noresle U dom S No S No dom U dom S dom S dom S dom S h dom S ¬ S suc h < s U dom S suc h ¬ S < s U dom S
103 10 6 14 15 101 102 syl23anc ¬ x A y A ¬ x < s y A No A V U A ¬ S < s U dom S