Step | Hyp | Ref
| Expression |
1 | | ltrelnq 6349 |
. . . . . 6
⊢
<Q ⊆ (Q ×
Q) |
2 | 1 | brel 4335 |
. . . . 5
⊢ (𝐶 <Q
B → (𝐶 ∈
Q ∧ B ∈
Q)) |
3 | 2 | simprd 107 |
. . . 4
⊢ (𝐶 <Q
B → B ∈
Q) |
4 | 3 | adantl 262 |
. . 3
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ 𝐶 ∈ 𝑈) ∧ 𝐶 <Q B) → B
∈ Q) |
5 | | breq2 3759 |
. . . . . . 7
⊢ (𝑏 = B → (𝐶 <Q 𝑏 ↔ 𝐶 <Q B)) |
6 | | eleq1 2097 |
. . . . . . 7
⊢ (𝑏 = B → (𝑏 ∈ 𝑈 ↔ B ∈ 𝑈)) |
7 | 5, 6 | imbi12d 223 |
. . . . . 6
⊢ (𝑏 = B → ((𝐶 <Q 𝑏 → 𝑏 ∈ 𝑈) ↔ (𝐶 <Q B → B ∈ 𝑈))) |
8 | 7 | imbi2d 219 |
. . . . 5
⊢ (𝑏 = B → (((〈𝐿, 𝑈〉 ∈
P ∧ 𝐶 ∈ 𝑈) → (𝐶 <Q 𝑏 → 𝑏 ∈ 𝑈)) ↔ ((〈𝐿, 𝑈〉 ∈
P ∧ 𝐶 ∈ 𝑈) → (𝐶 <Q B → B ∈ 𝑈)))) |
9 | 1 | brel 4335 |
. . . . . . . 8
⊢ (𝐶 <Q
𝑏 → (𝐶 ∈
Q ∧ 𝑏 ∈
Q)) |
10 | | an42 521 |
. . . . . . . . 9
⊢ (((𝐶 ∈ Q ∧ 𝑏
∈ Q) ∧ (𝐶 ∈ 𝑈 ∧ 〈𝐿, 𝑈〉 ∈
P)) ↔ ((𝐶 ∈
Q ∧ 𝐶 ∈ 𝑈) ∧ (〈𝐿, 𝑈〉 ∈
P ∧ 𝑏 ∈
Q))) |
11 | | breq1 3758 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝐶 → (𝑐 <Q 𝑏 ↔ 𝐶 <Q 𝑏)) |
12 | | eleq1 2097 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝐶 → (𝑐 ∈ 𝑈 ↔ 𝐶 ∈ 𝑈)) |
13 | 11, 12 | anbi12d 442 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝐶 → ((𝑐 <Q 𝑏 ∧
𝑐 ∈ 𝑈) ↔ (𝐶 <Q 𝑏 ∧
𝐶 ∈ 𝑈))) |
14 | 13 | rspcev 2650 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ Q ∧ (𝐶 <Q 𝑏 ∧
𝐶 ∈ 𝑈)) → ∃𝑐 ∈
Q (𝑐
<Q 𝑏 ∧ 𝑐 ∈ 𝑈)) |
15 | | elinp 6457 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝐿, 𝑈〉 ∈ P ↔ (((𝐿 ⊆ Q ∧ 𝑈 ⊆ Q) ∧ (∃𝑐 ∈ Q 𝑐 ∈ 𝐿 ∧ ∃𝑏 ∈ Q 𝑏 ∈ 𝑈)) ∧ ((∀𝑐 ∈ Q (𝑐 ∈ 𝐿 ↔ ∃𝑏 ∈
Q (𝑐
<Q 𝑏 ∧ 𝑏 ∈ 𝐿)) ∧ ∀𝑏 ∈
Q (𝑏 ∈ 𝑈 ↔ ∃𝑐 ∈
Q (𝑐
<Q 𝑏 ∧ 𝑐 ∈ 𝑈))) ∧ ∀𝑐 ∈
Q ¬ (𝑐 ∈ 𝐿 ∧ 𝑐 ∈ 𝑈) ∧ ∀𝑐 ∈
Q ∀𝑏 ∈
Q (𝑐
<Q 𝑏 → (𝑐 ∈ 𝐿
∨ 𝑏 ∈ 𝑈))))) |
16 | | simpr1r 961 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐿 ⊆ Q ∧ 𝑈 ⊆ Q) ∧ (∃𝑐 ∈ Q 𝑐 ∈ 𝐿 ∧ ∃𝑏 ∈ Q 𝑏 ∈ 𝑈)) ∧ ((∀𝑐 ∈ Q (𝑐 ∈ 𝐿 ↔ ∃𝑏 ∈
Q (𝑐
<Q 𝑏 ∧ 𝑏 ∈ 𝐿)) ∧ ∀𝑏 ∈
Q (𝑏 ∈ 𝑈 ↔ ∃𝑐 ∈
Q (𝑐
<Q 𝑏 ∧ 𝑐 ∈ 𝑈))) ∧ ∀𝑐 ∈
Q ¬ (𝑐 ∈ 𝐿 ∧ 𝑐 ∈ 𝑈) ∧ ∀𝑐 ∈
Q ∀𝑏 ∈
Q (𝑐
<Q 𝑏 → (𝑐 ∈ 𝐿
∨ 𝑏 ∈ 𝑈)))) → ∀𝑏 ∈
Q (𝑏 ∈ 𝑈 ↔ ∃𝑐 ∈
Q (𝑐
<Q 𝑏 ∧ 𝑐 ∈ 𝑈))) |
17 | 15, 16 | sylbi 114 |
. . . . . . . . . . . . . . 15
⊢
(〈𝐿, 𝑈〉 ∈ P → ∀𝑏 ∈
Q (𝑏 ∈ 𝑈 ↔ ∃𝑐 ∈
Q (𝑐
<Q 𝑏 ∧ 𝑐 ∈ 𝑈))) |
18 | 17 | r19.21bi 2401 |
. . . . . . . . . . . . . 14
⊢
((〈𝐿, 𝑈〉 ∈ P ∧ 𝑏
∈ Q) → (𝑏 ∈ 𝑈 ↔ ∃𝑐 ∈
Q (𝑐
<Q 𝑏 ∧ 𝑐 ∈ 𝑈))) |
19 | 14, 18 | syl5ibrcom 146 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ Q ∧ (𝐶 <Q 𝑏 ∧
𝐶 ∈ 𝑈)) → ((〈𝐿, 𝑈〉 ∈
P ∧ 𝑏 ∈
Q) → 𝑏
∈ 𝑈)) |
20 | 19 | 3impb 1099 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ Q ∧ 𝐶 <Q 𝑏 ∧
𝐶 ∈ 𝑈) → ((〈𝐿, 𝑈〉 ∈
P ∧ 𝑏 ∈
Q) → 𝑏
∈ 𝑈)) |
21 | 20 | 3com12 1107 |
. . . . . . . . . . 11
⊢ ((𝐶 <Q
𝑏 ∧ 𝐶 ∈
Q ∧ 𝐶 ∈ 𝑈) → ((〈𝐿, 𝑈〉 ∈
P ∧ 𝑏 ∈
Q) → 𝑏
∈ 𝑈)) |
22 | 21 | 3expib 1106 |
. . . . . . . . . 10
⊢ (𝐶 <Q
𝑏 → ((𝐶 ∈
Q ∧ 𝐶 ∈ 𝑈) → ((〈𝐿, 𝑈〉 ∈
P ∧ 𝑏 ∈
Q) → 𝑏
∈ 𝑈))) |
23 | 22 | impd 242 |
. . . . . . . . 9
⊢ (𝐶 <Q
𝑏 → (((𝐶 ∈
Q ∧ 𝐶 ∈ 𝑈) ∧ (〈𝐿, 𝑈〉 ∈
P ∧ 𝑏 ∈
Q)) → 𝑏
∈ 𝑈)) |
24 | 10, 23 | syl5bi 141 |
. . . . . . . 8
⊢ (𝐶 <Q
𝑏 → (((𝐶 ∈
Q ∧ 𝑏 ∈
Q) ∧ (𝐶 ∈ 𝑈 ∧ 〈𝐿, 𝑈〉 ∈
P)) → 𝑏
∈ 𝑈)) |
25 | 9, 24 | mpand 405 |
. . . . . . 7
⊢ (𝐶 <Q
𝑏 → ((𝐶 ∈ 𝑈 ∧ 〈𝐿, 𝑈〉 ∈
P) → 𝑏
∈ 𝑈)) |
26 | 25 | com12 27 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑈 ∧
〈𝐿, 𝑈〉 ∈
P) → (𝐶
<Q 𝑏 → 𝑏 ∈ 𝑈)) |
27 | 26 | ancoms 255 |
. . . . 5
⊢
((〈𝐿, 𝑈〉 ∈ P ∧ 𝐶 ∈ 𝑈) → (𝐶 <Q 𝑏 → 𝑏 ∈ 𝑈)) |
28 | 8, 27 | vtoclg 2607 |
. . . 4
⊢ (B ∈
Q → ((〈𝐿, 𝑈〉 ∈
P ∧ 𝐶 ∈ 𝑈) → (𝐶 <Q B → B ∈ 𝑈))) |
29 | 28 | impd 242 |
. . 3
⊢ (B ∈
Q → (((〈𝐿, 𝑈〉 ∈
P ∧ 𝐶 ∈ 𝑈) ∧ 𝐶 <Q B) → B
∈ 𝑈)) |
30 | 4, 29 | mpcom 32 |
. 2
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ 𝐶 ∈ 𝑈) ∧ 𝐶 <Q B) → B
∈ 𝑈) |
31 | 30 | ex 108 |
1
⊢
((〈𝐿, 𝑈〉 ∈ P ∧ 𝐶 ∈ 𝑈) → (𝐶 <Q B → B ∈ 𝑈)) |