Step | Hyp | Ref
| Expression |
1 | | nsmallnq 9799 |
. . . . 5
⊢ (𝐴 ∈ Q →
∃𝑥 𝑥 <Q 𝐴) |
2 | | abn0 3954 |
. . . . 5
⊢ ({𝑥 ∣ 𝑥 <Q 𝐴} ≠ ∅ ↔
∃𝑥 𝑥 <Q 𝐴) |
3 | 1, 2 | sylibr 224 |
. . . 4
⊢ (𝐴 ∈ Q →
{𝑥 ∣ 𝑥 <Q
𝐴} ≠
∅) |
4 | | 0pss 4013 |
. . . 4
⊢ (∅
⊊ {𝑥 ∣ 𝑥 <Q
𝐴} ↔ {𝑥 ∣ 𝑥 <Q 𝐴} ≠ ∅) |
5 | 3, 4 | sylibr 224 |
. . 3
⊢ (𝐴 ∈ Q →
∅ ⊊ {𝑥 ∣
𝑥
<Q 𝐴}) |
6 | | ltrelnq 9748 |
. . . . . . 7
⊢
<Q ⊆ (Q ×
Q) |
7 | 6 | brel 5168 |
. . . . . 6
⊢ (𝑥 <Q
𝐴 → (𝑥 ∈ Q ∧
𝐴 ∈
Q)) |
8 | 7 | simpld 475 |
. . . . 5
⊢ (𝑥 <Q
𝐴 → 𝑥 ∈ Q) |
9 | 8 | abssi 3677 |
. . . 4
⊢ {𝑥 ∣ 𝑥 <Q 𝐴} ⊆
Q |
10 | | ltsonq 9791 |
. . . . . . 7
⊢
<Q Or Q |
11 | 10, 6 | soirri 5522 |
. . . . . 6
⊢ ¬
𝐴
<Q 𝐴 |
12 | | breq1 4656 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 <Q 𝐴 ↔ 𝐴 <Q 𝐴)) |
13 | 12 | elabg 3351 |
. . . . . 6
⊢ (𝐴 ∈ Q →
(𝐴 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ↔ 𝐴 <Q 𝐴)) |
14 | 11, 13 | mtbiri 317 |
. . . . 5
⊢ (𝐴 ∈ Q →
¬ 𝐴 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) |
15 | 14 | ancli 574 |
. . . 4
⊢ (𝐴 ∈ Q →
(𝐴 ∈ Q
∧ ¬ 𝐴 ∈ {𝑥 ∣ 𝑥 <Q 𝐴})) |
16 | | ssnelpss 3718 |
. . . 4
⊢ ({𝑥 ∣ 𝑥 <Q 𝐴} ⊆ Q →
((𝐴 ∈ Q
∧ ¬ 𝐴 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) → {𝑥 ∣ 𝑥 <Q 𝐴} ⊊
Q)) |
17 | 9, 15, 16 | mpsyl 68 |
. . 3
⊢ (𝐴 ∈ Q →
{𝑥 ∣ 𝑥 <Q
𝐴} ⊊
Q) |
18 | 5, 17 | jca 554 |
. 2
⊢ (𝐴 ∈ Q →
(∅ ⊊ {𝑥
∣ 𝑥
<Q 𝐴} ∧ {𝑥 ∣ 𝑥 <Q 𝐴} ⊊
Q)) |
19 | | vex 3203 |
. . . . 5
⊢ 𝑦 ∈ V |
20 | | breq1 4656 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 <Q 𝐴 ↔ 𝑦 <Q 𝐴)) |
21 | 19, 20 | elab 3350 |
. . . 4
⊢ (𝑦 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ↔ 𝑦 <Q 𝐴) |
22 | 10, 6 | sotri 5523 |
. . . . . . . . 9
⊢ ((𝑧 <Q
𝑦 ∧ 𝑦 <Q 𝐴) → 𝑧 <Q 𝐴) |
23 | 22 | expcom 451 |
. . . . . . . 8
⊢ (𝑦 <Q
𝐴 → (𝑧 <Q
𝑦 → 𝑧 <Q 𝐴)) |
24 | 23 | adantl 482 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝑦
<Q 𝐴) → (𝑧 <Q 𝑦 → 𝑧 <Q 𝐴)) |
25 | | vex 3203 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
26 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 <Q 𝐴 ↔ 𝑧 <Q 𝐴)) |
27 | 25, 26 | elab 3350 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ↔ 𝑧 <Q 𝐴) |
28 | 24, 27 | syl6ibr 242 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝑦
<Q 𝐴) → (𝑧 <Q 𝑦 → 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴})) |
29 | 28 | alrimiv 1855 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝑦
<Q 𝐴) → ∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴})) |
30 | | ltbtwnnq 9800 |
. . . . . . . 8
⊢ (𝑦 <Q
𝐴 ↔ ∃𝑧(𝑦 <Q 𝑧 ∧ 𝑧 <Q 𝐴)) |
31 | 27 | anbi2i 730 |
. . . . . . . . . . 11
⊢ ((𝑦 <Q
𝑧 ∧ 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) ↔ (𝑦 <Q 𝑧 ∧ 𝑧 <Q 𝐴)) |
32 | 31 | biimpri 218 |
. . . . . . . . . 10
⊢ ((𝑦 <Q
𝑧 ∧ 𝑧 <Q 𝐴) → (𝑦 <Q 𝑧 ∧ 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴})) |
33 | 32 | ancomd 467 |
. . . . . . . . 9
⊢ ((𝑦 <Q
𝑧 ∧ 𝑧 <Q 𝐴) → (𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∧ 𝑦 <Q 𝑧)) |
34 | 33 | eximi 1762 |
. . . . . . . 8
⊢
(∃𝑧(𝑦 <Q
𝑧 ∧ 𝑧 <Q 𝐴) → ∃𝑧(𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∧ 𝑦 <Q 𝑧)) |
35 | 30, 34 | sylbi 207 |
. . . . . . 7
⊢ (𝑦 <Q
𝐴 → ∃𝑧(𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∧ 𝑦 <Q 𝑧)) |
36 | 35 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝑦
<Q 𝐴) → ∃𝑧(𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∧ 𝑦 <Q 𝑧)) |
37 | | df-rex 2918 |
. . . . . 6
⊢
(∃𝑧 ∈
{𝑥 ∣ 𝑥 <Q
𝐴}𝑦 <Q 𝑧 ↔ ∃𝑧(𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∧ 𝑦 <Q 𝑧)) |
38 | 36, 37 | sylibr 224 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝑦
<Q 𝐴) → ∃𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}𝑦 <Q 𝑧) |
39 | 29, 38 | jca 554 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝑦
<Q 𝐴) → (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) ∧ ∃𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}𝑦 <Q 𝑧)) |
40 | 21, 39 | sylan2b 492 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝑦 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) → (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) ∧ ∃𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}𝑦 <Q 𝑧)) |
41 | 40 | ralrimiva 2966 |
. 2
⊢ (𝐴 ∈ Q →
∀𝑦 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) ∧ ∃𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}𝑦 <Q 𝑧)) |
42 | | elnp 9809 |
. 2
⊢ ({𝑥 ∣ 𝑥 <Q 𝐴} ∈ P ↔
((∅ ⊊ {𝑥
∣ 𝑥
<Q 𝐴} ∧ {𝑥 ∣ 𝑥 <Q 𝐴} ⊊ Q)
∧ ∀𝑦 ∈
{𝑥 ∣ 𝑥 <Q
𝐴} (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) ∧ ∃𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}𝑦 <Q 𝑧))) |
43 | 18, 41, 42 | sylanbrc 698 |
1
⊢ (𝐴 ∈ Q →
{𝑥 ∣ 𝑥 <Q
𝐴} ∈
P) |