Proof of Theorem suplocexprlemru
Step | Hyp | Ref
| Expression |
1 | | suplocexpr.m |
. . . . . . . . . . . 12
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) |
2 | | suplocexpr.ub |
. . . . . . . . . . . 12
⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) |
3 | | suplocexpr.loc |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P
𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦))) |
4 | 1, 2, 3 | suplocexprlemss 7636 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ P) |
5 | | suplocexpr.b |
. . . . . . . . . . . 12
⊢ 𝐵 = 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}〉 |
6 | 5 | suplocexprlem2b 7635 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ P →
(2nd ‘𝐵) =
{𝑢 ∈ Q
∣ ∃𝑤 ∈
∩ (2nd “ 𝐴)𝑤 <Q 𝑢}) |
7 | 4, 6 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → (2nd
‘𝐵) = {𝑢 ∈ Q ∣
∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}) |
8 | 7 | eleq2d 2227 |
. . . . . . . . 9
⊢ (𝜑 → (𝑟 ∈ (2nd ‘𝐵) ↔ 𝑟 ∈ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢})) |
9 | 8 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ Q) → (𝑟 ∈ (2nd
‘𝐵) ↔ 𝑟 ∈ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢})) |
10 | 9 | biimpa 294 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑟 ∈ (2nd
‘𝐵)) → 𝑟 ∈ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}) |
11 | | breq2 3970 |
. . . . . . . . 9
⊢ (𝑢 = 𝑟 → (𝑤 <Q 𝑢 ↔ 𝑤 <Q 𝑟)) |
12 | 11 | rexbidv 2458 |
. . . . . . . 8
⊢ (𝑢 = 𝑟 → (∃𝑤 ∈ ∩
(2nd “ 𝐴)𝑤 <Q 𝑢 ↔ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑟)) |
13 | 12 | elrab 2868 |
. . . . . . 7
⊢ (𝑟 ∈ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢} ↔ (𝑟 ∈ Q ∧ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑟)) |
14 | 10, 13 | sylib 121 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑟 ∈ (2nd
‘𝐵)) → (𝑟 ∈ Q ∧
∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑟)) |
15 | 14 | simprd 113 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑟 ∈ (2nd
‘𝐵)) →
∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑟) |
16 | | ltbtwnnqq 7336 |
. . . . . . . 8
⊢ (𝑤 <Q
𝑟 ↔ ∃𝑞 ∈ Q (𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟)) |
17 | 16 | biimpi 119 |
. . . . . . 7
⊢ (𝑤 <Q
𝑟 → ∃𝑞 ∈ Q (𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟)) |
18 | 17 | ad2antll 483 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) → ∃𝑞 ∈ Q (𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟)) |
19 | | simprr 522 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞 ∈ Q) ∧ (𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟)) → 𝑞 <Q 𝑟) |
20 | | breq2 3970 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑞 → (𝑤 <Q 𝑢 ↔ 𝑤 <Q 𝑞)) |
21 | 20 | rexbidv 2458 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑞 → (∃𝑤 ∈ ∩
(2nd “ 𝐴)𝑤 <Q 𝑢 ↔ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑞)) |
22 | | simplr 520 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞 ∈ Q) ∧ (𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟)) → 𝑞 ∈ Q) |
23 | | simprl 521 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) → 𝑤 ∈ ∩
(2nd “ 𝐴)) |
24 | 23 | ad2antrr 480 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞 ∈ Q) ∧ (𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟)) → 𝑤 ∈ ∩
(2nd “ 𝐴)) |
25 | | simprl 521 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞 ∈ Q) ∧ (𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟)) → 𝑤 <Q 𝑞) |
26 | 24, 25 | jca 304 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞 ∈ Q) ∧ (𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟)) → (𝑤 ∈ ∩
(2nd “ 𝐴)
∧ 𝑤
<Q 𝑞)) |
27 | | rspe 2506 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑞) → ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑞) |
28 | 26, 27 | syl 14 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞 ∈ Q) ∧ (𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟)) → ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑞) |
29 | 21, 22, 28 | elrabd 2870 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞 ∈ Q) ∧ (𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟)) → 𝑞 ∈ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}) |
30 | 7 | eleq2d 2227 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑞 ∈ (2nd ‘𝐵) ↔ 𝑞 ∈ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢})) |
31 | 30 | ad5antr 488 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞 ∈ Q) ∧ (𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟)) → (𝑞 ∈ (2nd ‘𝐵) ↔ 𝑞 ∈ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢})) |
32 | 29, 31 | mpbird 166 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞 ∈ Q) ∧ (𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟)) → 𝑞 ∈ (2nd ‘𝐵)) |
33 | 19, 32 | jca 304 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞 ∈ Q) ∧ (𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟)) → (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) |
34 | 33 | ex 114 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞 ∈ Q) → ((𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟) → (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵)))) |
35 | 34 | reximdva 2559 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) → (∃𝑞 ∈ Q (𝑤 <Q
𝑞 ∧ 𝑞 <Q 𝑟) → ∃𝑞 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵)))) |
36 | 18, 35 | mpd 13 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑟 ∈ (2nd
‘𝐵)) ∧ (𝑤 ∈ ∩ (2nd “ 𝐴) ∧ 𝑤 <Q 𝑟)) → ∃𝑞 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) |
37 | 15, 36 | rexlimddv 2579 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑟 ∈ (2nd
‘𝐵)) →
∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) |
38 | 37 | ex 114 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ Q) → (𝑟 ∈ (2nd
‘𝐵) →
∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵)))) |
39 | | simpllr 524 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧
(𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) → 𝑟 ∈ Q) |
40 | | simprr 522 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧
(𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) → 𝑞 ∈ (2nd ‘𝐵)) |
41 | 30 | ad3antrrr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧
(𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) → (𝑞 ∈ (2nd ‘𝐵) ↔ 𝑞 ∈ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢})) |
42 | 40, 41 | mpbid 146 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧
(𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) → 𝑞 ∈ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}) |
43 | 21 | elrab 2868 |
. . . . . . . . 9
⊢ (𝑞 ∈ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢} ↔ (𝑞 ∈ Q ∧ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑞)) |
44 | 42, 43 | sylib 121 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧
(𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) → (𝑞 ∈ Q ∧ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑞)) |
45 | 44 | simprd 113 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧
(𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) → ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑞) |
46 | | simpr 109 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑞 ∈ Q)
∧ (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) ∧ 𝑤 ∈ ∩
(2nd “ 𝐴))
∧ 𝑤
<Q 𝑞) → 𝑤 <Q 𝑞) |
47 | | simprl 521 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧
(𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) → 𝑞 <Q 𝑟) |
48 | 47 | ad2antrr 480 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑞 ∈ Q)
∧ (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) ∧ 𝑤 ∈ ∩
(2nd “ 𝐴))
∧ 𝑤
<Q 𝑞) → 𝑞 <Q 𝑟) |
49 | 46, 48 | jca 304 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑞 ∈ Q)
∧ (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) ∧ 𝑤 ∈ ∩
(2nd “ 𝐴))
∧ 𝑤
<Q 𝑞) → (𝑤 <Q 𝑞 ∧ 𝑞 <Q 𝑟)) |
50 | | ltrelnq 7286 |
. . . . . . . . . . . . . 14
⊢
<Q ⊆ (Q ×
Q) |
51 | 50 | brel 4639 |
. . . . . . . . . . . . 13
⊢ (𝑤 <Q
𝑞 → (𝑤 ∈ Q ∧
𝑞 ∈
Q)) |
52 | 51 | simpld 111 |
. . . . . . . . . . . 12
⊢ (𝑤 <Q
𝑞 → 𝑤 ∈ Q) |
53 | 52 | adantl 275 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑞 ∈ Q)
∧ (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) ∧ 𝑤 ∈ ∩
(2nd “ 𝐴))
∧ 𝑤
<Q 𝑞) → 𝑤 ∈ Q) |
54 | | simp-4r 532 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑞 ∈ Q)
∧ (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) ∧ 𝑤 ∈ ∩
(2nd “ 𝐴))
∧ 𝑤
<Q 𝑞) → 𝑞 ∈ Q) |
55 | 39 | ad2antrr 480 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑞 ∈ Q)
∧ (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) ∧ 𝑤 ∈ ∩
(2nd “ 𝐴))
∧ 𝑤
<Q 𝑞) → 𝑟 ∈ Q) |
56 | | ltsonq 7319 |
. . . . . . . . . . . 12
⊢
<Q Or Q |
57 | | sotr 4279 |
. . . . . . . . . . . 12
⊢ ((
<Q Or Q ∧ (𝑤 ∈ Q ∧ 𝑞 ∈ Q ∧
𝑟 ∈ Q))
→ ((𝑤
<Q 𝑞 ∧ 𝑞 <Q 𝑟) → 𝑤 <Q 𝑟)) |
58 | 56, 57 | mpan 421 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ Q ∧
𝑞 ∈ Q
∧ 𝑟 ∈
Q) → ((𝑤
<Q 𝑞 ∧ 𝑞 <Q 𝑟) → 𝑤 <Q 𝑟)) |
59 | 53, 54, 55, 58 | syl3anc 1220 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑞 ∈ Q)
∧ (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) ∧ 𝑤 ∈ ∩
(2nd “ 𝐴))
∧ 𝑤
<Q 𝑞) → ((𝑤 <Q 𝑞 ∧ 𝑞 <Q 𝑟) → 𝑤 <Q 𝑟)) |
60 | 49, 59 | mpd 13 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑞 ∈ Q)
∧ (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) ∧ 𝑤 ∈ ∩
(2nd “ 𝐴))
∧ 𝑤
<Q 𝑞) → 𝑤 <Q 𝑟) |
61 | 60 | ex 114 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ Q) ∧
𝑞 ∈ Q)
∧ (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) ∧ 𝑤 ∈ ∩
(2nd “ 𝐴))
→ (𝑤
<Q 𝑞 → 𝑤 <Q 𝑟)) |
62 | 61 | reximdva 2559 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧
(𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) → (∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑞 → ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑟)) |
63 | 45, 62 | mpd 13 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧
(𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) → ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑟) |
64 | 12, 39, 63 | elrabd 2870 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧
(𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) → 𝑟 ∈ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}) |
65 | 8 | ad3antrrr 484 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧
(𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) → (𝑟 ∈ (2nd ‘𝐵) ↔ 𝑟 ∈ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢})) |
66 | 64, 65 | mpbird 166 |
. . . 4
⊢ ((((𝜑 ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧
(𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) → 𝑟 ∈ (2nd ‘𝐵)) |
67 | 66 | rexlimdva2 2577 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ Q) → (∃𝑞 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵)) → 𝑟 ∈ (2nd ‘𝐵))) |
68 | 38, 67 | impbid 128 |
. 2
⊢ ((𝜑 ∧ 𝑟 ∈ Q) → (𝑟 ∈ (2nd
‘𝐵) ↔
∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵)))) |
69 | 68 | ralrimiva 2530 |
1
⊢ (𝜑 → ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐵) ↔ ∃𝑞 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵)))) |