Proof of Theorem nqprloc
Step | Hyp | Ref
| Expression |
1 | | nqtri3or 7318 |
. . . . . . 7
⊢ ((𝑞 ∈ Q ∧
𝐴 ∈ Q)
→ (𝑞
<Q 𝐴 ∨ 𝑞 = 𝐴 ∨ 𝐴 <Q 𝑞)) |
2 | 1 | ancoms 266 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝑞 ∈ Q)
→ (𝑞
<Q 𝐴 ∨ 𝑞 = 𝐴 ∨ 𝐴 <Q 𝑞)) |
3 | 2 | ad2antrr 480 |
. . . . 5
⊢ ((((𝐴 ∈ Q ∧
𝑞 ∈ Q)
∧ 𝑟 ∈
Q) ∧ 𝑞
<Q 𝑟) → (𝑞 <Q 𝐴 ∨ 𝑞 = 𝐴 ∨ 𝐴 <Q 𝑞)) |
4 | | vex 2715 |
. . . . . . . . . 10
⊢ 𝑞 ∈ V |
5 | | breq1 3970 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑞 → (𝑥 <Q 𝐴 ↔ 𝑞 <Q 𝐴)) |
6 | 4, 5 | elab 2856 |
. . . . . . . . 9
⊢ (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ↔ 𝑞 <Q 𝐴) |
7 | 6 | biimpri 132 |
. . . . . . . 8
⊢ (𝑞 <Q
𝐴 → 𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) |
8 | 7 | orcd 723 |
. . . . . . 7
⊢ (𝑞 <Q
𝐴 → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥})) |
9 | 8 | a1i 9 |
. . . . . 6
⊢ ((((𝐴 ∈ Q ∧
𝑞 ∈ Q)
∧ 𝑟 ∈
Q) ∧ 𝑞
<Q 𝑟) → (𝑞 <Q 𝐴 → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))) |
10 | | simpr 109 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Q ∧
𝑞 ∈ Q)
∧ 𝑟 ∈
Q) ∧ 𝑞
<Q 𝑟) → 𝑞 <Q 𝑟) |
11 | | breq1 3970 |
. . . . . . . 8
⊢ (𝑞 = 𝐴 → (𝑞 <Q 𝑟 ↔ 𝐴 <Q 𝑟)) |
12 | 10, 11 | syl5ibcom 154 |
. . . . . . 7
⊢ ((((𝐴 ∈ Q ∧
𝑞 ∈ Q)
∧ 𝑟 ∈
Q) ∧ 𝑞
<Q 𝑟) → (𝑞 = 𝐴 → 𝐴 <Q 𝑟)) |
13 | | vex 2715 |
. . . . . . . . 9
⊢ 𝑟 ∈ V |
14 | | breq2 3971 |
. . . . . . . . 9
⊢ (𝑥 = 𝑟 → (𝐴 <Q 𝑥 ↔ 𝐴 <Q 𝑟)) |
15 | 13, 14 | elab 2856 |
. . . . . . . 8
⊢ (𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥} ↔ 𝐴 <Q 𝑟) |
16 | | olc 701 |
. . . . . . . 8
⊢ (𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥} → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥})) |
17 | 15, 16 | sylbir 134 |
. . . . . . 7
⊢ (𝐴 <Q
𝑟 → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥})) |
18 | 12, 17 | syl6 33 |
. . . . . 6
⊢ ((((𝐴 ∈ Q ∧
𝑞 ∈ Q)
∧ 𝑟 ∈
Q) ∧ 𝑞
<Q 𝑟) → (𝑞 = 𝐴 → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))) |
19 | | ltsonq 7320 |
. . . . . . . . . 10
⊢
<Q Or Q |
20 | | ltrelnq 7287 |
. . . . . . . . . 10
⊢
<Q ⊆ (Q ×
Q) |
21 | 19, 20 | sotri 4983 |
. . . . . . . . 9
⊢ ((𝐴 <Q
𝑞 ∧ 𝑞 <Q 𝑟) → 𝐴 <Q 𝑟) |
22 | 21, 17 | syl 14 |
. . . . . . . 8
⊢ ((𝐴 <Q
𝑞 ∧ 𝑞 <Q 𝑟) → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥})) |
23 | 22 | expcom 115 |
. . . . . . 7
⊢ (𝑞 <Q
𝑟 → (𝐴 <Q 𝑞 → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))) |
24 | 23 | adantl 275 |
. . . . . 6
⊢ ((((𝐴 ∈ Q ∧
𝑞 ∈ Q)
∧ 𝑟 ∈
Q) ∧ 𝑞
<Q 𝑟) → (𝐴 <Q 𝑞 → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))) |
25 | 9, 18, 24 | 3jaod 1286 |
. . . . 5
⊢ ((((𝐴 ∈ Q ∧
𝑞 ∈ Q)
∧ 𝑟 ∈
Q) ∧ 𝑞
<Q 𝑟) → ((𝑞 <Q 𝐴 ∨ 𝑞 = 𝐴 ∨ 𝐴 <Q 𝑞) → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))) |
26 | 3, 25 | mpd 13 |
. . . 4
⊢ ((((𝐴 ∈ Q ∧
𝑞 ∈ Q)
∧ 𝑟 ∈
Q) ∧ 𝑞
<Q 𝑟) → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥})) |
27 | 26 | ex 114 |
. . 3
⊢ (((𝐴 ∈ Q ∧
𝑞 ∈ Q)
∧ 𝑟 ∈
Q) → (𝑞
<Q 𝑟 → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))) |
28 | 27 | ralrimiva 2530 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝑞 ∈ Q)
→ ∀𝑟 ∈
Q (𝑞
<Q 𝑟 → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))) |
29 | 28 | ralrimiva 2530 |
1
⊢ (𝐴 ∈ Q →
∀𝑞 ∈
Q ∀𝑟
∈ Q (𝑞
<Q 𝑟 → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))) |