Step | Hyp | Ref
| Expression |
1 | | suplocexprlemell 7635 |
. . . . . . 7
⊢ (𝑞 ∈ ∪ (1st “ 𝐴) ↔ ∃𝑠 ∈ 𝐴 𝑞 ∈ (1st ‘𝑠)) |
2 | 1 | biimpi 119 |
. . . . . 6
⊢ (𝑞 ∈ ∪ (1st “ 𝐴) → ∃𝑠 ∈ 𝐴 𝑞 ∈ (1st ‘𝑠)) |
3 | 2 | adantl 275 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ Q) ∧ 𝑞 ∈ ∪ (1st “ 𝐴)) → ∃𝑠 ∈ 𝐴 𝑞 ∈ (1st ‘𝑠)) |
4 | | suplocexpr.m |
. . . . . . . . . . 11
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) |
5 | | suplocexpr.ub |
. . . . . . . . . . 11
⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) |
6 | | suplocexpr.loc |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P
𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦))) |
7 | 4, 5, 6 | suplocexprlemss 7637 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ P) |
8 | 7 | ad3antrrr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ 𝑞 ∈ ∪ (1st “ 𝐴)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) → 𝐴 ⊆ P) |
9 | | simprl 521 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ 𝑞 ∈ ∪ (1st “ 𝐴)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) → 𝑠 ∈ 𝐴) |
10 | 8, 9 | sseldd 3129 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ 𝑞 ∈ ∪ (1st “ 𝐴)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) → 𝑠 ∈ P) |
11 | | prop 7397 |
. . . . . . . 8
⊢ (𝑠 ∈ P →
〈(1st ‘𝑠), (2nd ‘𝑠)〉 ∈
P) |
12 | 10, 11 | syl 14 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ 𝑞 ∈ ∪ (1st “ 𝐴)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) → 〈(1st
‘𝑠), (2nd
‘𝑠)〉 ∈
P) |
13 | | simprr 522 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ 𝑞 ∈ ∪ (1st “ 𝐴)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) → 𝑞 ∈ (1st ‘𝑠)) |
14 | | prnmaxl 7410 |
. . . . . . 7
⊢
((〈(1st ‘𝑠), (2nd ‘𝑠)〉 ∈ P ∧ 𝑞 ∈ (1st
‘𝑠)) →
∃𝑟 ∈
(1st ‘𝑠)𝑞 <Q 𝑟) |
15 | 12, 13, 14 | syl2anc 409 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ 𝑞 ∈ ∪ (1st “ 𝐴)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) → ∃𝑟 ∈ (1st
‘𝑠)𝑞 <Q 𝑟) |
16 | | ltrelnq 7287 |
. . . . . . . . 9
⊢
<Q ⊆ (Q ×
Q) |
17 | 16 | brel 4640 |
. . . . . . . 8
⊢ (𝑞 <Q
𝑟 → (𝑞 ∈ Q ∧
𝑟 ∈
Q)) |
18 | 17 | simprd 113 |
. . . . . . 7
⊢ (𝑞 <Q
𝑟 → 𝑟 ∈ Q) |
19 | 18 | ad2antll 483 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑞 ∈ Q) ∧
𝑞 ∈ ∪ (1st “ 𝐴)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) ∧ (𝑟 ∈ (1st ‘𝑠) ∧ 𝑞 <Q 𝑟)) → 𝑟 ∈ Q) |
20 | | simprr 522 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑞 ∈ Q) ∧
𝑞 ∈ ∪ (1st “ 𝐴)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) ∧ (𝑟 ∈ (1st ‘𝑠) ∧ 𝑞 <Q 𝑟)) → 𝑞 <Q 𝑟) |
21 | | simplrl 525 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑞 ∈ Q) ∧
𝑞 ∈ ∪ (1st “ 𝐴)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) ∧ (𝑟 ∈ (1st ‘𝑠) ∧ 𝑞 <Q 𝑟)) → 𝑠 ∈ 𝐴) |
22 | | simprl 521 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑞 ∈ Q) ∧
𝑞 ∈ ∪ (1st “ 𝐴)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) ∧ (𝑟 ∈ (1st ‘𝑠) ∧ 𝑞 <Q 𝑟)) → 𝑟 ∈ (1st ‘𝑠)) |
23 | | rspe 2506 |
. . . . . . . . 9
⊢ ((𝑠 ∈ 𝐴 ∧ 𝑟 ∈ (1st ‘𝑠)) → ∃𝑠 ∈ 𝐴 𝑟 ∈ (1st ‘𝑠)) |
24 | 21, 22, 23 | syl2anc 409 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑞 ∈ Q) ∧
𝑞 ∈ ∪ (1st “ 𝐴)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) ∧ (𝑟 ∈ (1st ‘𝑠) ∧ 𝑞 <Q 𝑟)) → ∃𝑠 ∈ 𝐴 𝑟 ∈ (1st ‘𝑠)) |
25 | | suplocexprlemell 7635 |
. . . . . . . 8
⊢ (𝑟 ∈ ∪ (1st “ 𝐴) ↔ ∃𝑠 ∈ 𝐴 𝑟 ∈ (1st ‘𝑠)) |
26 | 24, 25 | sylibr 133 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑞 ∈ Q) ∧
𝑞 ∈ ∪ (1st “ 𝐴)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) ∧ (𝑟 ∈ (1st ‘𝑠) ∧ 𝑞 <Q 𝑟)) → 𝑟 ∈ ∪
(1st “ 𝐴)) |
27 | 20, 26 | jca 304 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑞 ∈ Q) ∧
𝑞 ∈ ∪ (1st “ 𝐴)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) ∧ (𝑟 ∈ (1st ‘𝑠) ∧ 𝑞 <Q 𝑟)) → (𝑞 <Q 𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) |
28 | 15, 19, 27 | reximssdv 2561 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ 𝑞 ∈ ∪ (1st “ 𝐴)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) → ∃𝑟 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) |
29 | 3, 28 | rexlimddv 2579 |
. . . 4
⊢ (((𝜑 ∧ 𝑞 ∈ Q) ∧ 𝑞 ∈ ∪ (1st “ 𝐴)) → ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) |
30 | 29 | ex 114 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ Q) → (𝑞 ∈ ∪ (1st “ 𝐴) → ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴)))) |
31 | | simprr 522 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) → 𝑟 ∈ ∪
(1st “ 𝐴)) |
32 | 31, 25 | sylib 121 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) → ∃𝑠 ∈ 𝐴 𝑟 ∈ (1st ‘𝑠)) |
33 | | simprl 521 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ (𝑠 ∈ 𝐴 ∧ 𝑟 ∈ (1st ‘𝑠))) → 𝑠 ∈ 𝐴) |
34 | | simplrl 525 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ (𝑠 ∈ 𝐴 ∧ 𝑟 ∈ (1st ‘𝑠))) → 𝑞 <Q 𝑟) |
35 | 7 | ad3antrrr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ (𝑠 ∈ 𝐴 ∧ 𝑟 ∈ (1st ‘𝑠))) → 𝐴 ⊆ P) |
36 | 35, 33 | sseldd 3129 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ (𝑠 ∈ 𝐴 ∧ 𝑟 ∈ (1st ‘𝑠))) → 𝑠 ∈ P) |
37 | 36, 11 | syl 14 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ (𝑠 ∈ 𝐴 ∧ 𝑟 ∈ (1st ‘𝑠))) → 〈(1st
‘𝑠), (2nd
‘𝑠)〉 ∈
P) |
38 | | simprr 522 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ (𝑠 ∈ 𝐴 ∧ 𝑟 ∈ (1st ‘𝑠))) → 𝑟 ∈ (1st ‘𝑠)) |
39 | | prcdnql 7406 |
. . . . . . . . . . 11
⊢
((〈(1st ‘𝑠), (2nd ‘𝑠)〉 ∈ P ∧ 𝑟 ∈ (1st
‘𝑠)) → (𝑞 <Q
𝑟 → 𝑞 ∈ (1st ‘𝑠))) |
40 | 37, 38, 39 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ (𝑠 ∈ 𝐴 ∧ 𝑟 ∈ (1st ‘𝑠))) → (𝑞 <Q 𝑟 → 𝑞 ∈ (1st ‘𝑠))) |
41 | 34, 40 | mpd 13 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ (𝑠 ∈ 𝐴 ∧ 𝑟 ∈ (1st ‘𝑠))) → 𝑞 ∈ (1st ‘𝑠)) |
42 | | 19.8a 1570 |
. . . . . . . . 9
⊢ ((𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠)) → ∃𝑠(𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) |
43 | 33, 41, 42 | syl2anc 409 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ (𝑠 ∈ 𝐴 ∧ 𝑟 ∈ (1st ‘𝑠))) → ∃𝑠(𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) |
44 | | df-rex 2441 |
. . . . . . . 8
⊢
(∃𝑠 ∈
𝐴 𝑞 ∈ (1st ‘𝑠) ↔ ∃𝑠(𝑠 ∈ 𝐴 ∧ 𝑞 ∈ (1st ‘𝑠))) |
45 | 43, 44 | sylibr 133 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ (𝑠 ∈ 𝐴 ∧ 𝑟 ∈ (1st ‘𝑠))) → ∃𝑠 ∈ 𝐴 𝑞 ∈ (1st ‘𝑠)) |
46 | 45, 1 | sylibr 133 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ (𝑠 ∈ 𝐴 ∧ 𝑟 ∈ (1st ‘𝑠))) → 𝑞 ∈ ∪
(1st “ 𝐴)) |
47 | 32, 46 | rexlimddv 2579 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) → 𝑞 ∈ ∪
(1st “ 𝐴)) |
48 | 47 | ex 114 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ Q) → ((𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))
→ 𝑞 ∈ ∪ (1st “ 𝐴))) |
49 | 48 | rexlimdvw 2578 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ Q) → (∃𝑟 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))
→ 𝑞 ∈ ∪ (1st “ 𝐴))) |
50 | 30, 49 | impbid 128 |
. 2
⊢ ((𝜑 ∧ 𝑞 ∈ Q) → (𝑞 ∈ ∪ (1st “ 𝐴) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴)))) |
51 | 50 | ralrimiva 2530 |
1
⊢ (𝜑 → ∀𝑞 ∈ Q (𝑞 ∈ ∪
(1st “ 𝐴)
↔ ∃𝑟 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴)))) |