Step | Hyp | Ref
| Expression |
1 | | ltrelnq 7314 |
. . . . . 6
⊢
<Q ⊆ (Q ×
Q) |
2 | 1 | brel 4661 |
. . . . 5
⊢ (𝐶 <Q
𝐵 → (𝐶 ∈ Q ∧ 𝐵 ∈
Q)) |
3 | 2 | simprd 113 |
. . . 4
⊢ (𝐶 <Q
𝐵 → 𝐵 ∈ Q) |
4 | 3 | adantl 275 |
. . 3
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐶 ∈ 𝑈) ∧ 𝐶 <Q 𝐵) → 𝐵 ∈ Q) |
5 | | breq2 3991 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (𝐶 <Q 𝑏 ↔ 𝐶 <Q 𝐵)) |
6 | | eleq1 2233 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (𝑏 ∈ 𝑈 ↔ 𝐵 ∈ 𝑈)) |
7 | 5, 6 | imbi12d 233 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((𝐶 <Q 𝑏 → 𝑏 ∈ 𝑈) ↔ (𝐶 <Q 𝐵 → 𝐵 ∈ 𝑈))) |
8 | 7 | imbi2d 229 |
. . . . 5
⊢ (𝑏 = 𝐵 → (((〈𝐿, 𝑈〉 ∈ P ∧ 𝐶 ∈ 𝑈) → (𝐶 <Q 𝑏 → 𝑏 ∈ 𝑈)) ↔ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝐶 ∈ 𝑈) → (𝐶 <Q 𝐵 → 𝐵 ∈ 𝑈)))) |
9 | 1 | brel 4661 |
. . . . . . . 8
⊢ (𝐶 <Q
𝑏 → (𝐶 ∈ Q ∧ 𝑏 ∈
Q)) |
10 | | an42 582 |
. . . . . . . . 9
⊢ (((𝐶 ∈ Q ∧
𝑏 ∈ Q)
∧ (𝐶 ∈ 𝑈 ∧ 〈𝐿, 𝑈〉 ∈ P)) ↔
((𝐶 ∈ Q
∧ 𝐶 ∈ 𝑈) ∧ (〈𝐿, 𝑈〉 ∈ P ∧ 𝑏 ∈
Q))) |
11 | | breq1 3990 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝐶 → (𝑐 <Q 𝑏 ↔ 𝐶 <Q 𝑏)) |
12 | | eleq1 2233 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝐶 → (𝑐 ∈ 𝑈 ↔ 𝐶 ∈ 𝑈)) |
13 | 11, 12 | anbi12d 470 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝐶 → ((𝑐 <Q 𝑏 ∧ 𝑐 ∈ 𝑈) ↔ (𝐶 <Q 𝑏 ∧ 𝐶 ∈ 𝑈))) |
14 | 13 | rspcev 2834 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ Q ∧
(𝐶
<Q 𝑏 ∧ 𝐶 ∈ 𝑈)) → ∃𝑐 ∈ Q (𝑐 <Q 𝑏 ∧ 𝑐 ∈ 𝑈)) |
15 | | elinp 7423 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝐿, 𝑈〉 ∈ P
↔ (((𝐿 ⊆
Q ∧ 𝑈
⊆ Q) ∧ (∃𝑐 ∈ Q 𝑐 ∈ 𝐿 ∧ ∃𝑏 ∈ Q 𝑏 ∈ 𝑈)) ∧ ((∀𝑐 ∈ Q (𝑐 ∈ 𝐿 ↔ ∃𝑏 ∈ Q (𝑐 <Q 𝑏 ∧ 𝑏 ∈ 𝐿)) ∧ ∀𝑏 ∈ Q (𝑏 ∈ 𝑈 ↔ ∃𝑐 ∈ Q (𝑐 <Q 𝑏 ∧ 𝑐 ∈ 𝑈))) ∧ ∀𝑐 ∈ Q ¬ (𝑐 ∈ 𝐿 ∧ 𝑐 ∈ 𝑈) ∧ ∀𝑐 ∈ Q ∀𝑏 ∈ Q (𝑐 <Q
𝑏 → (𝑐 ∈ 𝐿 ∨ 𝑏 ∈ 𝑈))))) |
16 | | simpr1r 1050 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐿 ⊆ Q ∧
𝑈 ⊆ Q)
∧ (∃𝑐 ∈
Q 𝑐 ∈
𝐿 ∧ ∃𝑏 ∈ Q 𝑏 ∈ 𝑈)) ∧ ((∀𝑐 ∈ Q (𝑐 ∈ 𝐿 ↔ ∃𝑏 ∈ Q (𝑐 <Q 𝑏 ∧ 𝑏 ∈ 𝐿)) ∧ ∀𝑏 ∈ Q (𝑏 ∈ 𝑈 ↔ ∃𝑐 ∈ Q (𝑐 <Q 𝑏 ∧ 𝑐 ∈ 𝑈))) ∧ ∀𝑐 ∈ Q ¬ (𝑐 ∈ 𝐿 ∧ 𝑐 ∈ 𝑈) ∧ ∀𝑐 ∈ Q ∀𝑏 ∈ Q (𝑐 <Q
𝑏 → (𝑐 ∈ 𝐿 ∨ 𝑏 ∈ 𝑈)))) → ∀𝑏 ∈ Q (𝑏 ∈ 𝑈 ↔ ∃𝑐 ∈ Q (𝑐 <Q 𝑏 ∧ 𝑐 ∈ 𝑈))) |
17 | 15, 16 | sylbi 120 |
. . . . . . . . . . . . . . 15
⊢
(〈𝐿, 𝑈〉 ∈ P
→ ∀𝑏 ∈
Q (𝑏 ∈
𝑈 ↔ ∃𝑐 ∈ Q (𝑐 <Q
𝑏 ∧ 𝑐 ∈ 𝑈))) |
18 | 17 | r19.21bi 2558 |
. . . . . . . . . . . . . 14
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝑏 ∈
Q) → (𝑏
∈ 𝑈 ↔
∃𝑐 ∈
Q (𝑐
<Q 𝑏 ∧ 𝑐 ∈ 𝑈))) |
19 | 14, 18 | syl5ibrcom 156 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ Q ∧
(𝐶
<Q 𝑏 ∧ 𝐶 ∈ 𝑈)) → ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑏 ∈ Q) →
𝑏 ∈ 𝑈)) |
20 | 19 | 3impb 1194 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ Q ∧
𝐶
<Q 𝑏 ∧ 𝐶 ∈ 𝑈) → ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑏 ∈ Q) →
𝑏 ∈ 𝑈)) |
21 | 20 | 3com12 1202 |
. . . . . . . . . . 11
⊢ ((𝐶 <Q
𝑏 ∧ 𝐶 ∈ Q ∧ 𝐶 ∈ 𝑈) → ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑏 ∈ Q) →
𝑏 ∈ 𝑈)) |
22 | 21 | 3expib 1201 |
. . . . . . . . . 10
⊢ (𝐶 <Q
𝑏 → ((𝐶 ∈ Q ∧
𝐶 ∈ 𝑈) → ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑏 ∈ Q) →
𝑏 ∈ 𝑈))) |
23 | 22 | impd 252 |
. . . . . . . . 9
⊢ (𝐶 <Q
𝑏 → (((𝐶 ∈ Q ∧
𝐶 ∈ 𝑈) ∧ (〈𝐿, 𝑈〉 ∈ P ∧ 𝑏 ∈ Q)) →
𝑏 ∈ 𝑈)) |
24 | 10, 23 | syl5bi 151 |
. . . . . . . 8
⊢ (𝐶 <Q
𝑏 → (((𝐶 ∈ Q ∧
𝑏 ∈ Q)
∧ (𝐶 ∈ 𝑈 ∧ 〈𝐿, 𝑈〉 ∈ P)) → 𝑏 ∈ 𝑈)) |
25 | 9, 24 | mpand 427 |
. . . . . . 7
⊢ (𝐶 <Q
𝑏 → ((𝐶 ∈ 𝑈 ∧ 〈𝐿, 𝑈〉 ∈ P) → 𝑏 ∈ 𝑈)) |
26 | 25 | com12 30 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑈 ∧ 〈𝐿, 𝑈〉 ∈ P) → (𝐶 <Q
𝑏 → 𝑏 ∈ 𝑈)) |
27 | 26 | ancoms 266 |
. . . . 5
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐶 ∈ 𝑈) → (𝐶 <Q 𝑏 → 𝑏 ∈ 𝑈)) |
28 | 8, 27 | vtoclg 2790 |
. . . 4
⊢ (𝐵 ∈ Q →
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐶 ∈ 𝑈) → (𝐶 <Q 𝐵 → 𝐵 ∈ 𝑈))) |
29 | 28 | impd 252 |
. . 3
⊢ (𝐵 ∈ Q →
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐶 ∈ 𝑈) ∧ 𝐶 <Q 𝐵) → 𝐵 ∈ 𝑈)) |
30 | 4, 29 | mpcom 36 |
. 2
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐶 ∈ 𝑈) ∧ 𝐶 <Q 𝐵) → 𝐵 ∈ 𝑈) |
31 | 30 | ex 114 |
1
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐶 ∈ 𝑈) → (𝐶 <Q 𝐵 → 𝐵 ∈ 𝑈)) |