Step | Hyp | Ref
| Expression |
1 | | suplocexpr.b |
. . 3
⊢ 𝐵 = 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}〉 |
2 | | suplocexpr.m |
. . . . . 6
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) |
3 | | suplocexpr.ub |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) |
4 | | suplocexpr.loc |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P
𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦))) |
5 | 2, 3, 4 | suplocexprlemss 7664 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ P) |
6 | 1 | suplocexprlem2b 7663 |
. . . . 5
⊢ (𝐴 ⊆ P →
(2nd ‘𝐵) =
{𝑢 ∈ Q
∣ ∃𝑤 ∈
∩ (2nd “ 𝐴)𝑤 <Q 𝑢}) |
7 | 5, 6 | syl 14 |
. . . 4
⊢ (𝜑 → (2nd
‘𝐵) = {𝑢 ∈ Q ∣
∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}) |
8 | 7 | opeq2d 3770 |
. . 3
⊢ (𝜑 → 〈∪ (1st “ 𝐴), (2nd ‘𝐵)〉 = 〈∪
(1st “ 𝐴),
{𝑢 ∈ Q
∣ ∃𝑤 ∈
∩ (2nd “ 𝐴)𝑤 <Q 𝑢}〉) |
9 | 1, 8 | eqtr4id 2222 |
. 2
⊢ (𝜑 → 𝐵 = 〈∪
(1st “ 𝐴),
(2nd ‘𝐵)〉) |
10 | | suplocexprlemell 7662 |
. . . . . . . . 9
⊢ (𝑠 ∈ ∪ (1st “ 𝐴) ↔ ∃𝑡 ∈ 𝐴 𝑠 ∈ (1st ‘𝑡)) |
11 | 10 | biimpi 119 |
. . . . . . . 8
⊢ (𝑠 ∈ ∪ (1st “ 𝐴) → ∃𝑡 ∈ 𝐴 𝑠 ∈ (1st ‘𝑡)) |
12 | 11 | adantl 275 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
→ ∃𝑡 ∈
𝐴 𝑠 ∈ (1st ‘𝑡)) |
13 | 5 | ad2antrr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
∧ (𝑡 ∈ 𝐴 ∧ 𝑠 ∈ (1st ‘𝑡))) → 𝐴 ⊆ P) |
14 | | simprl 526 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
∧ (𝑡 ∈ 𝐴 ∧ 𝑠 ∈ (1st ‘𝑡))) → 𝑡 ∈ 𝐴) |
15 | 13, 14 | sseldd 3148 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
∧ (𝑡 ∈ 𝐴 ∧ 𝑠 ∈ (1st ‘𝑡))) → 𝑡 ∈ P) |
16 | | prop 7424 |
. . . . . . . . 9
⊢ (𝑡 ∈ P →
〈(1st ‘𝑡), (2nd ‘𝑡)〉 ∈
P) |
17 | 15, 16 | syl 14 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
∧ (𝑡 ∈ 𝐴 ∧ 𝑠 ∈ (1st ‘𝑡))) → 〈(1st
‘𝑡), (2nd
‘𝑡)〉 ∈
P) |
18 | | simprr 527 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
∧ (𝑡 ∈ 𝐴 ∧ 𝑠 ∈ (1st ‘𝑡))) → 𝑠 ∈ (1st ‘𝑡)) |
19 | | elprnql 7430 |
. . . . . . . 8
⊢
((〈(1st ‘𝑡), (2nd ‘𝑡)〉 ∈ P ∧ 𝑠 ∈ (1st
‘𝑡)) → 𝑠 ∈
Q) |
20 | 17, 18, 19 | syl2anc 409 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
∧ (𝑡 ∈ 𝐴 ∧ 𝑠 ∈ (1st ‘𝑡))) → 𝑠 ∈ Q) |
21 | 12, 20 | rexlimddv 2592 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
→ 𝑠 ∈
Q) |
22 | 21 | ex 114 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ ∪
(1st “ 𝐴)
→ 𝑠 ∈
Q)) |
23 | 22 | ssrdv 3153 |
. . . 4
⊢ (𝜑 → ∪ (1st “ 𝐴) ⊆ Q) |
24 | | ssrab2 3232 |
. . . . 5
⊢ {𝑢 ∈ Q ∣
∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢} ⊆
Q |
25 | 7, 24 | eqsstrdi 3199 |
. . . 4
⊢ (𝜑 → (2nd
‘𝐵) ⊆
Q) |
26 | 2, 3, 4 | suplocexprlemml 7665 |
. . . . 5
⊢ (𝜑 → ∃𝑞 ∈ Q 𝑞 ∈ ∪
(1st “ 𝐴)) |
27 | 2, 3, 4, 1 | suplocexprlemmu 7667 |
. . . . 5
⊢ (𝜑 → ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐵)) |
28 | 26, 27 | jca 304 |
. . . 4
⊢ (𝜑 → (∃𝑞 ∈ Q 𝑞 ∈ ∪
(1st “ 𝐴)
∧ ∃𝑟 ∈
Q 𝑟 ∈
(2nd ‘𝐵))) |
29 | 23, 25, 28 | jca31 307 |
. . 3
⊢ (𝜑 → ((∪ (1st “ 𝐴) ⊆ Q ∧
(2nd ‘𝐵)
⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ ∪
(1st “ 𝐴)
∧ ∃𝑟 ∈
Q 𝑟 ∈
(2nd ‘𝐵)))) |
30 | 2, 3, 4 | suplocexprlemrl 7666 |
. . . . 5
⊢ (𝜑 → ∀𝑞 ∈ Q (𝑞 ∈ ∪
(1st “ 𝐴)
↔ ∃𝑟 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴)))) |
31 | 2, 3, 4, 1 | suplocexprlemru 7668 |
. . . . 5
⊢ (𝜑 → ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐵) ↔ ∃𝑞 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵)))) |
32 | 30, 31 | jca 304 |
. . . 4
⊢ (𝜑 → (∀𝑞 ∈ Q (𝑞 ∈ ∪ (1st “ 𝐴) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐵) ↔ ∃𝑞 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))))) |
33 | 2, 3, 4, 1 | suplocexprlemdisj 7669 |
. . . 4
⊢ (𝜑 → ∀𝑞 ∈ Q ¬ (𝑞 ∈ ∪ (1st “ 𝐴) ∧ 𝑞 ∈ (2nd ‘𝐵))) |
34 | 2, 3, 4, 1 | suplocexprlemloc 7670 |
. . . 4
⊢ (𝜑 → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q
𝑟 → (𝑞 ∈ ∪ (1st “ 𝐴) ∨ 𝑟 ∈ (2nd ‘𝐵)))) |
35 | 32, 33, 34 | 3jca 1172 |
. . 3
⊢ (𝜑 → ((∀𝑞 ∈ Q (𝑞 ∈ ∪ (1st “ 𝐴) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐵) ↔ ∃𝑞 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵)))) ∧ ∀𝑞 ∈ Q ¬
(𝑞 ∈ ∪ (1st “ 𝐴) ∧ 𝑞 ∈ (2nd ‘𝐵)) ∧ ∀𝑞 ∈ Q
∀𝑟 ∈
Q (𝑞
<Q 𝑟 → (𝑞 ∈ ∪
(1st “ 𝐴)
∨ 𝑟 ∈
(2nd ‘𝐵))))) |
36 | | elinp 7423 |
. . 3
⊢
(〈∪ (1st “ 𝐴), (2nd ‘𝐵)〉 ∈ P
↔ (((∪ (1st “ 𝐴) ⊆ Q ∧
(2nd ‘𝐵)
⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ ∪
(1st “ 𝐴)
∧ ∃𝑟 ∈
Q 𝑟 ∈
(2nd ‘𝐵)))
∧ ((∀𝑞 ∈
Q (𝑞 ∈
∪ (1st “ 𝐴) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐵) ↔ ∃𝑞 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵)))) ∧ ∀𝑞 ∈ Q ¬
(𝑞 ∈ ∪ (1st “ 𝐴) ∧ 𝑞 ∈ (2nd ‘𝐵)) ∧ ∀𝑞 ∈ Q
∀𝑟 ∈
Q (𝑞
<Q 𝑟 → (𝑞 ∈ ∪
(1st “ 𝐴)
∨ 𝑟 ∈
(2nd ‘𝐵)))))) |
37 | 29, 35, 36 | sylanbrc 415 |
. 2
⊢ (𝜑 → 〈∪ (1st “ 𝐴), (2nd ‘𝐵)〉 ∈
P) |
38 | 9, 37 | eqeltrd 2247 |
1
⊢ (𝜑 → 𝐵 ∈ P) |