Step | Hyp | Ref
| Expression |
1 | | elinp 7395 |
. . . 4
⊢
(〈𝐿, 𝑈〉 ∈ P
↔ (((𝐿 ⊆
Q ∧ 𝑈
⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ 𝐿 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑈)) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝐿)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑈))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝐿 ∧ 𝑞 ∈ 𝑈) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q
𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))))) |
2 | | simpr3 990 |
. . . 4
⊢ ((((𝐿 ⊆ Q ∧
𝑈 ⊆ Q)
∧ (∃𝑞 ∈
Q 𝑞 ∈
𝐿 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑈)) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝐿)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑈))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝐿 ∧ 𝑞 ∈ 𝑈) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q
𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))) → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q
𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) |
3 | 1, 2 | sylbi 120 |
. . 3
⊢
(〈𝐿, 𝑈〉 ∈ P
→ ∀𝑞 ∈
Q ∀𝑟
∈ Q (𝑞
<Q 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) |
4 | 3 | adantr 274 |
. 2
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q
𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) |
5 | | simpr 109 |
. 2
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) → 𝐴 <Q 𝐵) |
6 | | ltrelnq 7286 |
. . . . . . 7
⊢
<Q ⊆ (Q ×
Q) |
7 | 6 | brel 4639 |
. . . . . 6
⊢ (𝐴 <Q
𝐵 → (𝐴 ∈ Q ∧ 𝐵 ∈
Q)) |
8 | 7 | simpld 111 |
. . . . 5
⊢ (𝐴 <Q
𝐵 → 𝐴 ∈ Q) |
9 | 8 | adantl 275 |
. . . 4
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) → 𝐴 ∈ Q) |
10 | | simpr 109 |
. . . . . . 7
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) ∧ 𝑞 = 𝐴) → 𝑞 = 𝐴) |
11 | 10 | breq1d 3976 |
. . . . . 6
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) ∧ 𝑞 = 𝐴) → (𝑞 <Q 𝑟 ↔ 𝐴 <Q 𝑟)) |
12 | 10 | eleq1d 2226 |
. . . . . . 7
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) ∧ 𝑞 = 𝐴) → (𝑞 ∈ 𝐿 ↔ 𝐴 ∈ 𝐿)) |
13 | 12 | orbi1d 781 |
. . . . . 6
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) ∧ 𝑞 = 𝐴) → ((𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈) ↔ (𝐴 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) |
14 | 11, 13 | imbi12d 233 |
. . . . 5
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) ∧ 𝑞 = 𝐴) → ((𝑞 <Q 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)) ↔ (𝐴 <Q 𝑟 → (𝐴 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))) |
15 | 14 | ralbidv 2457 |
. . . 4
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) ∧ 𝑞 = 𝐴) → (∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)) ↔ ∀𝑟 ∈ Q (𝐴 <Q 𝑟 → (𝐴 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))) |
16 | 9, 15 | rspcdv 2819 |
. . 3
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) → (∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q
𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)) → ∀𝑟 ∈ Q (𝐴 <Q 𝑟 → (𝐴 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))) |
17 | 7 | simprd 113 |
. . . . 5
⊢ (𝐴 <Q
𝐵 → 𝐵 ∈ Q) |
18 | 17 | adantl 275 |
. . . 4
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) → 𝐵 ∈ Q) |
19 | | simpr 109 |
. . . . . 6
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) ∧ 𝑟 = 𝐵) → 𝑟 = 𝐵) |
20 | 19 | breq2d 3978 |
. . . . 5
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) ∧ 𝑟 = 𝐵) → (𝐴 <Q 𝑟 ↔ 𝐴 <Q 𝐵)) |
21 | 19 | eleq1d 2226 |
. . . . . 6
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) ∧ 𝑟 = 𝐵) → (𝑟 ∈ 𝑈 ↔ 𝐵 ∈ 𝑈)) |
22 | 21 | orbi2d 780 |
. . . . 5
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) ∧ 𝑟 = 𝐵) → ((𝐴 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈) ↔ (𝐴 ∈ 𝐿 ∨ 𝐵 ∈ 𝑈))) |
23 | 20, 22 | imbi12d 233 |
. . . 4
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) ∧ 𝑟 = 𝐵) → ((𝐴 <Q 𝑟 → (𝐴 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)) ↔ (𝐴 <Q 𝐵 → (𝐴 ∈ 𝐿 ∨ 𝐵 ∈ 𝑈)))) |
24 | 18, 23 | rspcdv 2819 |
. . 3
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) → (∀𝑟 ∈ Q (𝐴 <Q 𝑟 → (𝐴 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)) → (𝐴 <Q 𝐵 → (𝐴 ∈ 𝐿 ∨ 𝐵 ∈ 𝑈)))) |
25 | 16, 24 | syld 45 |
. 2
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) → (∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q
𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)) → (𝐴 <Q 𝐵 → (𝐴 ∈ 𝐿 ∨ 𝐵 ∈ 𝑈)))) |
26 | 4, 5, 25 | mp2d 47 |
1
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴
<Q 𝐵) → (𝐴 ∈ 𝐿 ∨ 𝐵 ∈ 𝑈)) |