Step | Hyp | Ref
| Expression |
1 | | nsmallnq 10393 |
. . . 4
⊢ (𝐴 ∈ Q →
∃𝑥 𝑥 <Q 𝐴) |
2 | | abn0 4336 |
. . . 4
⊢ ({𝑥 ∣ 𝑥 <Q 𝐴} ≠ ∅ ↔
∃𝑥 𝑥 <Q 𝐴) |
3 | 1, 2 | sylibr 236 |
. . 3
⊢ (𝐴 ∈ Q →
{𝑥 ∣ 𝑥 <Q
𝐴} ≠
∅) |
4 | | 0pss 4396 |
. . 3
⊢ (∅
⊊ {𝑥 ∣ 𝑥 <Q
𝐴} ↔ {𝑥 ∣ 𝑥 <Q 𝐴} ≠ ∅) |
5 | 3, 4 | sylibr 236 |
. 2
⊢ (𝐴 ∈ Q →
∅ ⊊ {𝑥 ∣
𝑥
<Q 𝐴}) |
6 | | ltrelnq 10342 |
. . . . . 6
⊢
<Q ⊆ (Q ×
Q) |
7 | 6 | brel 5612 |
. . . . 5
⊢ (𝑥 <Q
𝐴 → (𝑥 ∈ Q ∧
𝐴 ∈
Q)) |
8 | 7 | simpld 497 |
. . . 4
⊢ (𝑥 <Q
𝐴 → 𝑥 ∈ Q) |
9 | 8 | abssi 4046 |
. . 3
⊢ {𝑥 ∣ 𝑥 <Q 𝐴} ⊆
Q |
10 | | ltsonq 10385 |
. . . . . 6
⊢
<Q Or Q |
11 | 10, 6 | soirri 5981 |
. . . . 5
⊢ ¬
𝐴
<Q 𝐴 |
12 | | breq1 5062 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 <Q 𝐴 ↔ 𝐴 <Q 𝐴)) |
13 | 12 | elabg 3666 |
. . . . 5
⊢ (𝐴 ∈ Q →
(𝐴 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ↔ 𝐴 <Q 𝐴)) |
14 | 11, 13 | mtbiri 329 |
. . . 4
⊢ (𝐴 ∈ Q →
¬ 𝐴 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) |
15 | 14 | ancli 551 |
. . 3
⊢ (𝐴 ∈ Q →
(𝐴 ∈ Q
∧ ¬ 𝐴 ∈ {𝑥 ∣ 𝑥 <Q 𝐴})) |
16 | | ssnelpss 4088 |
. . 3
⊢ ({𝑥 ∣ 𝑥 <Q 𝐴} ⊆ Q →
((𝐴 ∈ Q
∧ ¬ 𝐴 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) → {𝑥 ∣ 𝑥 <Q 𝐴} ⊊
Q)) |
17 | 9, 15, 16 | mpsyl 68 |
. 2
⊢ (𝐴 ∈ Q →
{𝑥 ∣ 𝑥 <Q
𝐴} ⊊
Q) |
18 | | vex 3498 |
. . . . 5
⊢ 𝑦 ∈ V |
19 | | breq1 5062 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 <Q 𝐴 ↔ 𝑦 <Q 𝐴)) |
20 | 18, 19 | elab 3667 |
. . . 4
⊢ (𝑦 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ↔ 𝑦 <Q 𝐴) |
21 | 10, 6 | sotri 5982 |
. . . . . . . . 9
⊢ ((𝑧 <Q
𝑦 ∧ 𝑦 <Q 𝐴) → 𝑧 <Q 𝐴) |
22 | 21 | expcom 416 |
. . . . . . . 8
⊢ (𝑦 <Q
𝐴 → (𝑧 <Q
𝑦 → 𝑧 <Q 𝐴)) |
23 | 22 | adantl 484 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝑦
<Q 𝐴) → (𝑧 <Q 𝑦 → 𝑧 <Q 𝐴)) |
24 | | vex 3498 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
25 | | breq1 5062 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 <Q 𝐴 ↔ 𝑧 <Q 𝐴)) |
26 | 24, 25 | elab 3667 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ↔ 𝑧 <Q 𝐴) |
27 | 23, 26 | syl6ibr 254 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝑦
<Q 𝐴) → (𝑧 <Q 𝑦 → 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴})) |
28 | 27 | alrimiv 1924 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝑦
<Q 𝐴) → ∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴})) |
29 | | ltbtwnnq 10394 |
. . . . . . . 8
⊢ (𝑦 <Q
𝐴 ↔ ∃𝑧(𝑦 <Q 𝑧 ∧ 𝑧 <Q 𝐴)) |
30 | 26 | anbi2i 624 |
. . . . . . . . . . 11
⊢ ((𝑦 <Q
𝑧 ∧ 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) ↔ (𝑦 <Q 𝑧 ∧ 𝑧 <Q 𝐴)) |
31 | 30 | biimpri 230 |
. . . . . . . . . 10
⊢ ((𝑦 <Q
𝑧 ∧ 𝑧 <Q 𝐴) → (𝑦 <Q 𝑧 ∧ 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴})) |
32 | 31 | ancomd 464 |
. . . . . . . . 9
⊢ ((𝑦 <Q
𝑧 ∧ 𝑧 <Q 𝐴) → (𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∧ 𝑦 <Q 𝑧)) |
33 | 32 | eximi 1831 |
. . . . . . . 8
⊢
(∃𝑧(𝑦 <Q
𝑧 ∧ 𝑧 <Q 𝐴) → ∃𝑧(𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∧ 𝑦 <Q 𝑧)) |
34 | 29, 33 | sylbi 219 |
. . . . . . 7
⊢ (𝑦 <Q
𝐴 → ∃𝑧(𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∧ 𝑦 <Q 𝑧)) |
35 | 34 | adantl 484 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝑦
<Q 𝐴) → ∃𝑧(𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∧ 𝑦 <Q 𝑧)) |
36 | | df-rex 3144 |
. . . . . 6
⊢
(∃𝑧 ∈
{𝑥 ∣ 𝑥 <Q
𝐴}𝑦 <Q 𝑧 ↔ ∃𝑧(𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∧ 𝑦 <Q 𝑧)) |
37 | 35, 36 | sylibr 236 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝑦
<Q 𝐴) → ∃𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}𝑦 <Q 𝑧) |
38 | 28, 37 | jca 514 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝑦
<Q 𝐴) → (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) ∧ ∃𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}𝑦 <Q 𝑧)) |
39 | 20, 38 | sylan2b 595 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝑦 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) → (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) ∧ ∃𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}𝑦 <Q 𝑧)) |
40 | 39 | ralrimiva 3182 |
. 2
⊢ (𝐴 ∈ Q →
∀𝑦 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) ∧ ∃𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}𝑦 <Q 𝑧)) |
41 | | elnp 10403 |
. 2
⊢ ({𝑥 ∣ 𝑥 <Q 𝐴} ∈ P ↔
((∅ ⊊ {𝑥
∣ 𝑥
<Q 𝐴} ∧ {𝑥 ∣ 𝑥 <Q 𝐴} ⊊ Q)
∧ ∀𝑦 ∈
{𝑥 ∣ 𝑥 <Q
𝐴} (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}) ∧ ∃𝑧 ∈ {𝑥 ∣ 𝑥 <Q 𝐴}𝑦 <Q 𝑧))) |
42 | 5, 17, 40, 41 | syl21anbrc 1340 |
1
⊢ (𝐴 ∈ Q →
{𝑥 ∣ 𝑥 <Q
𝐴} ∈
P) |