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 7714 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ P) |
6 | 1 | suplocexprlem2b 7713 |
. . . . 5
⊢ (𝐴 ⊆ P →
(2nd ‘𝐵) =
{𝑢 ∈ Q
∣ ∃𝑤 ∈
∩ (2nd “ 𝐴)𝑤 <Q 𝑢}) |
7 | 5, 6 | syl 14 |
. . . 4
⊢ (𝜑 → (2nd
‘𝐵) = {𝑢 ∈ Q ∣
∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}) |
8 | 7 | opeq2d 3786 |
. . 3
⊢ (𝜑 → ⟨∪ (1st “ 𝐴), (2nd ‘𝐵)⟩ = ⟨∪
(1st “ 𝐴),
{𝑢 ∈ Q
∣ ∃𝑤 ∈
∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩) |
9 | 1, 8 | eqtr4id 2229 |
. 2
⊢ (𝜑 → 𝐵 = ⟨∪
(1st “ 𝐴),
(2nd ‘𝐵)⟩) |
10 | | suplocexprlemell 7712 |
. . . . . . . . 9
⊢ (𝑠 ∈ ∪ (1st “ 𝐴) ↔ ∃𝑡 ∈ 𝐴 𝑠 ∈ (1st ‘𝑡)) |
11 | 10 | biimpi 120 |
. . . . . . . 8
⊢ (𝑠 ∈ ∪ (1st “ 𝐴) → ∃𝑡 ∈ 𝐴 𝑠 ∈ (1st ‘𝑡)) |
12 | 11 | adantl 277 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
→ ∃𝑡 ∈
𝐴 𝑠 ∈ (1st ‘𝑡)) |
13 | 5 | ad2antrr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
∧ (𝑡 ∈ 𝐴 ∧ 𝑠 ∈ (1st ‘𝑡))) → 𝐴 ⊆ P) |
14 | | simprl 529 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
∧ (𝑡 ∈ 𝐴 ∧ 𝑠 ∈ (1st ‘𝑡))) → 𝑡 ∈ 𝐴) |
15 | 13, 14 | sseldd 3157 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
∧ (𝑡 ∈ 𝐴 ∧ 𝑠 ∈ (1st ‘𝑡))) → 𝑡 ∈ P) |
16 | | prop 7474 |
. . . . . . . . 9
⊢ (𝑡 ∈ P →
⟨(1st ‘𝑡), (2nd ‘𝑡)⟩ ∈
P) |
17 | 15, 16 | syl 14 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
∧ (𝑡 ∈ 𝐴 ∧ 𝑠 ∈ (1st ‘𝑡))) → ⟨(1st
‘𝑡), (2nd
‘𝑡)⟩ ∈
P) |
18 | | simprr 531 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
∧ (𝑡 ∈ 𝐴 ∧ 𝑠 ∈ (1st ‘𝑡))) → 𝑠 ∈ (1st ‘𝑡)) |
19 | | elprnql 7480 |
. . . . . . . 8
⊢
((⟨(1st ‘𝑡), (2nd ‘𝑡)⟩ ∈ P ∧ 𝑠 ∈ (1st
‘𝑡)) → 𝑠 ∈
Q) |
20 | 17, 18, 19 | syl2anc 411 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
∧ (𝑡 ∈ 𝐴 ∧ 𝑠 ∈ (1st ‘𝑡))) → 𝑠 ∈ Q) |
21 | 12, 20 | rexlimddv 2599 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ∪
(1st “ 𝐴))
→ 𝑠 ∈
Q) |
22 | 21 | ex 115 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ ∪
(1st “ 𝐴)
→ 𝑠 ∈
Q)) |
23 | 22 | ssrdv 3162 |
. . . 4
⊢ (𝜑 → ∪ (1st “ 𝐴) ⊆ Q) |
24 | | ssrab2 3241 |
. . . . 5
⊢ {𝑢 ∈ Q ∣
∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢} ⊆
Q |
25 | 7, 24 | eqsstrdi 3208 |
. . . 4
⊢ (𝜑 → (2nd
‘𝐵) ⊆
Q) |
26 | 2, 3, 4 | suplocexprlemml 7715 |
. . . . 5
⊢ (𝜑 → ∃𝑞 ∈ Q 𝑞 ∈ ∪
(1st “ 𝐴)) |
27 | 2, 3, 4, 1 | suplocexprlemmu 7717 |
. . . . 5
⊢ (𝜑 → ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐵)) |
28 | 26, 27 | jca 306 |
. . . 4
⊢ (𝜑 → (∃𝑞 ∈ Q 𝑞 ∈ ∪
(1st “ 𝐴)
∧ ∃𝑟 ∈
Q 𝑟 ∈
(2nd ‘𝐵))) |
29 | 23, 25, 28 | jca31 309 |
. . 3
⊢ (𝜑 → ((∪ (1st “ 𝐴) ⊆ Q ∧
(2nd ‘𝐵)
⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ ∪
(1st “ 𝐴)
∧ ∃𝑟 ∈
Q 𝑟 ∈
(2nd ‘𝐵)))) |
30 | 2, 3, 4 | suplocexprlemrl 7716 |
. . . . 5
⊢ (𝜑 → ∀𝑞 ∈ Q (𝑞 ∈ ∪
(1st “ 𝐴)
↔ ∃𝑟 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴)))) |
31 | 2, 3, 4, 1 | suplocexprlemru 7718 |
. . . . 5
⊢ (𝜑 → ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐵) ↔ ∃𝑞 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵)))) |
32 | 30, 31 | jca 306 |
. . . 4
⊢ (𝜑 → (∀𝑞 ∈ Q (𝑞 ∈ ∪ (1st “ 𝐴) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐵) ↔ ∃𝑞 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))))) |
33 | 2, 3, 4, 1 | suplocexprlemdisj 7719 |
. . . 4
⊢ (𝜑 → ∀𝑞 ∈ Q ¬ (𝑞 ∈ ∪ (1st “ 𝐴) ∧ 𝑞 ∈ (2nd ‘𝐵))) |
34 | 2, 3, 4, 1 | suplocexprlemloc 7720 |
. . . 4
⊢ (𝜑 → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q
𝑟 → (𝑞 ∈ ∪ (1st “ 𝐴) ∨ 𝑟 ∈ (2nd ‘𝐵)))) |
35 | 32, 33, 34 | 3jca 1177 |
. . 3
⊢ (𝜑 → ((∀𝑞 ∈ Q (𝑞 ∈ ∪ (1st “ 𝐴) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ ∪
(1st “ 𝐴))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐵) ↔ ∃𝑞 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵)))) ∧ ∀𝑞 ∈ Q ¬
(𝑞 ∈ ∪ (1st “ 𝐴) ∧ 𝑞 ∈ (2nd ‘𝐵)) ∧ ∀𝑞 ∈ Q
∀𝑟 ∈
Q (𝑞
<Q 𝑟 → (𝑞 ∈ ∪
(1st “ 𝐴)
∨ 𝑟 ∈
(2nd ‘𝐵))))) |
36 | | elinp 7473 |
. . 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 417 |
. 2
⊢ (𝜑 → ⟨∪ (1st “ 𝐴), (2nd ‘𝐵)⟩ ∈
P) |
38 | 9, 37 | eqeltrd 2254 |
1
⊢ (𝜑 → 𝐵 ∈ P) |