Step | Hyp | Ref
| Expression |
1 | | elprnql 7443 |
. . . . 5
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐵 ∈ 𝐿) → 𝐵 ∈ Q) |
2 | | elinp 7436 |
. . . . . . . 8
⊢
(〈𝐿, 𝑈〉 ∈ P
↔ (((𝐿 ⊆
Q ∧ 𝑈
⊆ Q) ∧ (∃𝑦 ∈ Q 𝑦 ∈ 𝐿 ∧ ∃𝑥 ∈ Q 𝑥 ∈ 𝑈)) ∧ ((∀𝑦 ∈ Q (𝑦 ∈ 𝐿 ↔ ∃𝑥 ∈ Q (𝑦 <Q 𝑥 ∧ 𝑥 ∈ 𝐿)) ∧ ∀𝑥 ∈ Q (𝑥 ∈ 𝑈 ↔ ∃𝑦 ∈ Q (𝑦 <Q 𝑥 ∧ 𝑦 ∈ 𝑈))) ∧ ∀𝑦 ∈ Q ¬ (𝑦 ∈ 𝐿 ∧ 𝑦 ∈ 𝑈) ∧ ∀𝑦 ∈ Q ∀𝑥 ∈ Q (𝑦 <Q
𝑥 → (𝑦 ∈ 𝐿 ∨ 𝑥 ∈ 𝑈))))) |
3 | | simpr1l 1049 |
. . . . . . . 8
⊢ ((((𝐿 ⊆ Q ∧
𝑈 ⊆ Q)
∧ (∃𝑦 ∈
Q 𝑦 ∈
𝐿 ∧ ∃𝑥 ∈ Q 𝑥 ∈ 𝑈)) ∧ ((∀𝑦 ∈ Q (𝑦 ∈ 𝐿 ↔ ∃𝑥 ∈ Q (𝑦 <Q 𝑥 ∧ 𝑥 ∈ 𝐿)) ∧ ∀𝑥 ∈ Q (𝑥 ∈ 𝑈 ↔ ∃𝑦 ∈ Q (𝑦 <Q 𝑥 ∧ 𝑦 ∈ 𝑈))) ∧ ∀𝑦 ∈ Q ¬ (𝑦 ∈ 𝐿 ∧ 𝑦 ∈ 𝑈) ∧ ∀𝑦 ∈ Q ∀𝑥 ∈ Q (𝑦 <Q
𝑥 → (𝑦 ∈ 𝐿 ∨ 𝑥 ∈ 𝑈)))) → ∀𝑦 ∈ Q (𝑦 ∈ 𝐿 ↔ ∃𝑥 ∈ Q (𝑦 <Q 𝑥 ∧ 𝑥 ∈ 𝐿))) |
4 | 2, 3 | sylbi 120 |
. . . . . . 7
⊢
(〈𝐿, 𝑈〉 ∈ P
→ ∀𝑦 ∈
Q (𝑦 ∈
𝐿 ↔ ∃𝑥 ∈ Q (𝑦 <Q
𝑥 ∧ 𝑥 ∈ 𝐿))) |
5 | | eleq1 2233 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → (𝑦 ∈ 𝐿 ↔ 𝐵 ∈ 𝐿)) |
6 | | breq1 3992 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐵 → (𝑦 <Q 𝑥 ↔ 𝐵 <Q 𝑥)) |
7 | 6 | anbi1d 462 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 → ((𝑦 <Q 𝑥 ∧ 𝑥 ∈ 𝐿) ↔ (𝐵 <Q 𝑥 ∧ 𝑥 ∈ 𝐿))) |
8 | 7 | rexbidv 2471 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ Q (𝑦 <Q 𝑥 ∧ 𝑥 ∈ 𝐿) ↔ ∃𝑥 ∈ Q (𝐵 <Q 𝑥 ∧ 𝑥 ∈ 𝐿))) |
9 | 5, 8 | bibi12d 234 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → ((𝑦 ∈ 𝐿 ↔ ∃𝑥 ∈ Q (𝑦 <Q 𝑥 ∧ 𝑥 ∈ 𝐿)) ↔ (𝐵 ∈ 𝐿 ↔ ∃𝑥 ∈ Q (𝐵 <Q 𝑥 ∧ 𝑥 ∈ 𝐿)))) |
10 | 9 | rspcv 2830 |
. . . . . . 7
⊢ (𝐵 ∈ Q →
(∀𝑦 ∈
Q (𝑦 ∈
𝐿 ↔ ∃𝑥 ∈ Q (𝑦 <Q
𝑥 ∧ 𝑥 ∈ 𝐿)) → (𝐵 ∈ 𝐿 ↔ ∃𝑥 ∈ Q (𝐵 <Q 𝑥 ∧ 𝑥 ∈ 𝐿)))) |
11 | | biimp 117 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝐿 ↔ ∃𝑥 ∈ Q (𝐵 <Q 𝑥 ∧ 𝑥 ∈ 𝐿)) → (𝐵 ∈ 𝐿 → ∃𝑥 ∈ Q (𝐵 <Q 𝑥 ∧ 𝑥 ∈ 𝐿))) |
12 | 4, 10, 11 | syl56 34 |
. . . . . 6
⊢ (𝐵 ∈ Q →
(〈𝐿, 𝑈〉 ∈ P → (𝐵 ∈ 𝐿 → ∃𝑥 ∈ Q (𝐵 <Q 𝑥 ∧ 𝑥 ∈ 𝐿)))) |
13 | 12 | impd 252 |
. . . . 5
⊢ (𝐵 ∈ Q →
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐵 ∈ 𝐿) → ∃𝑥 ∈ Q (𝐵 <Q
𝑥 ∧ 𝑥 ∈ 𝐿))) |
14 | 1, 13 | mpcom 36 |
. . . 4
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐵 ∈ 𝐿) → ∃𝑥 ∈ Q (𝐵 <Q
𝑥 ∧ 𝑥 ∈ 𝐿)) |
15 | | df-rex 2454 |
. . . 4
⊢
(∃𝑥 ∈
Q (𝐵
<Q 𝑥 ∧ 𝑥 ∈ 𝐿) ↔ ∃𝑥(𝑥 ∈ Q ∧ (𝐵 <Q
𝑥 ∧ 𝑥 ∈ 𝐿))) |
16 | 14, 15 | sylib 121 |
. . 3
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐵 ∈ 𝐿) → ∃𝑥(𝑥 ∈ Q ∧ (𝐵 <Q
𝑥 ∧ 𝑥 ∈ 𝐿))) |
17 | | ltrelnq 7327 |
. . . . . . . . 9
⊢
<Q ⊆ (Q ×
Q) |
18 | 17 | brel 4663 |
. . . . . . . 8
⊢ (𝐵 <Q
𝑥 → (𝐵 ∈ Q ∧ 𝑥 ∈
Q)) |
19 | 18 | simprd 113 |
. . . . . . 7
⊢ (𝐵 <Q
𝑥 → 𝑥 ∈ Q) |
20 | 19 | pm4.71ri 390 |
. . . . . 6
⊢ (𝐵 <Q
𝑥 ↔ (𝑥 ∈ Q ∧
𝐵
<Q 𝑥)) |
21 | 20 | anbi1i 455 |
. . . . 5
⊢ ((𝐵 <Q
𝑥 ∧ 𝑥 ∈ 𝐿) ↔ ((𝑥 ∈ Q ∧ 𝐵 <Q
𝑥) ∧ 𝑥 ∈ 𝐿)) |
22 | | ancom 264 |
. . . . 5
⊢ ((𝐵 <Q
𝑥 ∧ 𝑥 ∈ 𝐿) ↔ (𝑥 ∈ 𝐿 ∧ 𝐵 <Q 𝑥)) |
23 | | anass 399 |
. . . . 5
⊢ (((𝑥 ∈ Q ∧
𝐵
<Q 𝑥) ∧ 𝑥 ∈ 𝐿) ↔ (𝑥 ∈ Q ∧ (𝐵 <Q
𝑥 ∧ 𝑥 ∈ 𝐿))) |
24 | 21, 22, 23 | 3bitr3i 209 |
. . . 4
⊢ ((𝑥 ∈ 𝐿 ∧ 𝐵 <Q 𝑥) ↔ (𝑥 ∈ Q ∧ (𝐵 <Q
𝑥 ∧ 𝑥 ∈ 𝐿))) |
25 | 24 | exbii 1598 |
. . 3
⊢
(∃𝑥(𝑥 ∈ 𝐿 ∧ 𝐵 <Q 𝑥) ↔ ∃𝑥(𝑥 ∈ Q ∧ (𝐵 <Q
𝑥 ∧ 𝑥 ∈ 𝐿))) |
26 | 16, 25 | sylibr 133 |
. 2
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐵 ∈ 𝐿) → ∃𝑥(𝑥 ∈ 𝐿 ∧ 𝐵 <Q 𝑥)) |
27 | | df-rex 2454 |
. 2
⊢
(∃𝑥 ∈
𝐿 𝐵 <Q 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐿 ∧ 𝐵 <Q 𝑥)) |
28 | 26, 27 | sylibr 133 |
1
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐵 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 𝐵 <Q 𝑥) |