Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  axpre-suploclemres Unicode version

Theorem axpre-suploclemres 7702
 Description: Lemma for axpre-suploc 7703. The result. The proof just needs to define as basically the same set as (but expressed as a subset of rather than a subset of ), and apply suplocsr 7610. (Contributed by Jim Kingdon, 24-Jan-2024.)
Hypotheses
Ref Expression
axpre-suploclem.ss
axpre-suploclem.m
axpre-suploclem.ub
axpre-suploclem.loc
axpre-suploclem.b
Assertion
Ref Expression
axpre-suploclemres
Distinct variable groups:   ,,,   ,,,   ,,,   ,   ,,,
Allowed substitution hints:   ()   ()   (,,)

Proof of Theorem axpre-suploclemres
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axpre-suploclem.ss . . . . . . . 8
2 axpre-suploclem.m . . . . . . . 8
31, 2sseldd 3093 . . . . . . 7
4 elreal2 7631 . . . . . . 7
53, 4sylib 121 . . . . . 6
65simpld 111 . . . . 5
75simprd 113 . . . . . 6
87, 2eqeltrrd 2215 . . . . 5
9 opeq1 3700 . . . . . . 7
109eleq1d 2206 . . . . . 6
11 axpre-suploclem.b . . . . . 6
1210, 11elrab2 2838 . . . . 5
136, 8, 12sylanbrc 413 . . . 4
14 eleq1 2200 . . . . 5
1514spcegv 2769 . . . 4
1613, 13, 15sylc 62 . . 3
17 axpre-suploclem.ub . . . 4
18 simprl 520 . . . . . . 7
19 elreal2 7631 . . . . . . 7
2018, 19sylib 121 . . . . . 6
2120simpld 111 . . . . 5
22 breq1 3927 . . . . . . . . 9
23 simplrr 525 . . . . . . . . 9
24 simpr 109 . . . . . . . . . . 11
25 opeq1 3700 . . . . . . . . . . . . 13
2625eleq1d 2206 . . . . . . . . . . . 12
2726, 11elrab2 2838 . . . . . . . . . . 11
2824, 27sylib 121 . . . . . . . . . 10
2928simprd 113 . . . . . . . . 9
3022, 23, 29rspcdva 2789 . . . . . . . 8
31 simplrl 524 . . . . . . . . . 10
3231, 19sylib 121 . . . . . . . . 9
3332simprd 113 . . . . . . . 8
3430, 33breqtrd 3949 . . . . . . 7
35 ltresr 7640 . . . . . . 7
3634, 35sylib 121 . . . . . 6
3736ralrimiva 2503 . . . . 5
38 brralrspcev 3981 . . . . 5
3921, 37, 38syl2anc 408 . . . 4
4017, 39rexlimddv 2552 . . 3
41 simpr 109 . . . . . . . 8
42 ltresr 7640 . . . . . . . 8
4341, 42sylibr 133 . . . . . . 7
44 breq2 3928 . . . . . . . . 9
45 breq2 3928 . . . . . . . . . . 11
4645ralbidv 2435 . . . . . . . . . 10
4746orbi2d 779 . . . . . . . . 9
4844, 47imbi12d 233 . . . . . . . 8
49 breq1 3927 . . . . . . . . . . 11
50 breq1 3927 . . . . . . . . . . . . 13
5150rexbidv 2436 . . . . . . . . . . . 12
5251orbi1d 780 . . . . . . . . . . 11
5349, 52imbi12d 233 . . . . . . . . . 10
5453ralbidv 2435 . . . . . . . . 9
55 axpre-suploclem.loc . . . . . . . . . 10
5655ad2antrr 479 . . . . . . . . 9
57 simplrl 524 . . . . . . . . . 10
58 opelreal 7628 . . . . . . . . . 10
5957, 58sylibr 133 . . . . . . . . 9
6054, 56, 59rspcdva 2789 . . . . . . . 8
61 simplrr 525 . . . . . . . . 9
62 opelreal 7628 . . . . . . . . 9
6361, 62sylibr 133 . . . . . . . 8
6448, 60, 63rspcdva 2789 . . . . . . 7
6543, 64mpd 13 . . . . . 6
66 simplll 522 . . . . . . . . . . . . 13
67 simprl 520 . . . . . . . . . . . . 13
681sseld 3091 . . . . . . . . . . . . 13
6966, 67, 68sylc 62 . . . . . . . . . . . 12
70 elreal2 7631 . . . . . . . . . . . 12
7169, 70sylib 121 . . . . . . . . . . 11
7271simpld 111 . . . . . . . . . 10
7371simprd 113 . . . . . . . . . . 11
7473, 67eqeltrrd 2215 . . . . . . . . . 10
75 opeq1 3700 . . . . . . . . . . . 12
7675eleq1d 2206 . . . . . . . . . . 11
7776, 11elrab2 2838 . . . . . . . . . 10
7872, 74, 77sylanbrc 413 . . . . . . . . 9
79 simprr 521 . . . . . . . . . . 11
8079, 73breqtrd 3949 . . . . . . . . . 10
81 ltresr 7640 . . . . . . . . . 10
8280, 81sylib 121 . . . . . . . . 9
83 breq2 3928 . . . . . . . . . 10
8483rspcev 2784 . . . . . . . . 9
8578, 82, 84syl2anc 408 . . . . . . . 8
8685rexlimdvaa 2548 . . . . . . 7
87 breq1 3927 . . . . . . . . . . 11
88 simplr 519 . . . . . . . . . . 11
89 simpr 109 . . . . . . . . . . . . 13
90 opeq1 3700 . . . . . . . . . . . . . . 15
9190eleq1d 2206 . . . . . . . . . . . . . 14
9291, 11elrab2 2838 . . . . . . . . . . . . 13
9389, 92sylib 121 . . . . . . . . . . . 12
9493simprd 113 . . . . . . . . . . 11
9587, 88, 94rspcdva 2789 . . . . . . . . . 10
96 ltresr 7640 . . . . . . . . . 10
9795, 96sylib 121 . . . . . . . . 9
9897ralrimiva 2503 . . . . . . . 8
9998ex 114 . . . . . . 7
10086, 99orim12d 775 . . . . . 6
10165, 100mpd 13 . . . . 5
102101ex 114 . . . 4
103102ralrimivva 2512 . . 3
10416, 40, 103suplocsr 7610 . 2
105 simprl 520 . . . 4
106105, 58sylibr 133 . . 3
107 breq2 3928 . . . . . . . 8
108107notbid 656 . . . . . . 7
109 simplrr 525 . . . . . . 7
1101sselda 3092 . . . . . . . . . . 11
111 elreal2 7631 . . . . . . . . . . 11
112110, 111sylib 121 . . . . . . . . . 10
113112simpld 111 . . . . . . . . 9
114112simprd 113 . . . . . . . . . 10
115 simpr 109 . . . . . . . . . 10
116114, 115eqeltrrd 2215 . . . . . . . . 9
117 opeq1 3700 . . . . . . . . . . 11
118117eleq1d 2206 . . . . . . . . . 10
119118, 11elrab2 2838 . . . . . . . . 9
120113, 116, 119sylanbrc 413 . . . . . . . 8
121120adantlr 468 . . . . . . 7
122108, 109, 121rspcdva 2789 . . . . . 6
123114adantlr 468 . . . . . . . 8
124123breq2d 3936 . . . . . . 7
125 ltresr 7640 . . . . . . 7
126124, 125syl6bb 195 . . . . . 6
127122, 126mtbird 662 . . . . 5
128127ralrimiva 2503 . . . 4
130 simplr 519 . . . . . . . . . . . 12
131130, 111sylib 121 . . . . . . . . . . 11
132131simprd 113 . . . . . . . . . 10
133 simpr 109 . . . . . . . . . 10
134132, 133eqbrtrrd 3947 . . . . . . . . 9
135 ltresr 7640 . . . . . . . . 9
136134, 135sylib 121 . . . . . . . 8
137 breq1 3927 . . . . . . . . . 10
138 breq1 3927 . . . . . . . . . . 11
139138rexbidv 2436 . . . . . . . . . 10
140137, 139imbi12d 233 . . . . . . . . 9
141 simprr 521 . . . . . . . . . 10
142141ad2antrr 479 . . . . . . . . 9
143131simpld 111 . . . . . . . . 9
144140, 142, 143rspcdva 2789 . . . . . . . 8
145136, 144mpd 13 . . . . . . 7
146 nfv 1508 . . . . . . . . . . 11
147 nfv 1508 . . . . . . . . . . . 12
148 nfcv 2279 . . . . . . . . . . . . 13
149 nfv 1508 . . . . . . . . . . . . . 14
150 nfre1 2474 . . . . . . . . . . . . . 14
151149, 150nfim 1551 . . . . . . . . . . . . 13
152148, 151nfralya 2471 . . . . . . . . . . . 12
153147, 152nfan 1544 . . . . . . . . . . 11
154146, 153nfan 1544 . . . . . . . . . 10
155 nfv 1508 . . . . . . . . . 10
156154, 155nfan 1544 . . . . . . . . 9
157 nfv 1508 . . . . . . . . 9
158156, 157nfan 1544 . . . . . . . 8
159 nfv 1508 . . . . . . . 8
160 simprl 520 . . . . . . . . . . . 12
161160, 92sylib 121 . . . . . . . . . . 11
162161simprd 113 . . . . . . . . . 10
163132adantr 274 . . . . . . . . . . 11
164 simprr 521 . . . . . . . . . . . 12
165 ltresr 7640 . . . . . . . . . . . 12
166164, 165sylibr 133 . . . . . . . . . . 11
167163, 166eqbrtrd 3945 . . . . . . . . . 10
168 breq2 3928 . . . . . . . . . . 11
169168rspcev 2784 . . . . . . . . . 10
170162, 167, 169syl2anc 408 . . . . . . . . 9
171170exp32 362 . . . . . . . 8
172158, 159, 171rexlimd 2544 . . . . . . 7
173145, 172mpd 13 . . . . . 6
174173ex 114 . . . . 5
175174ralrimiva 2503 . . . 4