| Step | Hyp | Ref
| Expression |
| 1 | | prpssnq 11030 |
. . . . 5
⊢ (𝐴 ∈ P →
𝐴 ⊊
Q) |
| 2 | | pssnel 4471 |
. . . . 5
⊢ (𝐴 ⊊ Q →
∃𝑥(𝑥 ∈ Q ∧ ¬ 𝑥 ∈ 𝐴)) |
| 3 | | recclnq 11006 |
. . . . . . . . . 10
⊢ (𝑥 ∈ Q →
(*Q‘𝑥) ∈ Q) |
| 4 | | nsmallnq 11017 |
. . . . . . . . . 10
⊢
((*Q‘𝑥) ∈ Q → ∃𝑧 𝑧 <Q
(*Q‘𝑥)) |
| 5 | 3, 4 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ Q →
∃𝑧 𝑧 <Q
(*Q‘𝑥)) |
| 6 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝑥 ∈ Q ∧
¬ 𝑥 ∈ 𝐴) → ∃𝑧 𝑧 <Q
(*Q‘𝑥)) |
| 7 | | recrecnq 11007 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ Q →
(*Q‘(*Q‘𝑥)) = 𝑥) |
| 8 | 7 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ Q →
((*Q‘(*Q‘𝑥)) ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) |
| 9 | 8 | notbid 318 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ Q →
(¬
(*Q‘(*Q‘𝑥)) ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐴)) |
| 10 | 9 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ Q →
((𝑧
<Q (*Q‘𝑥) ∧ ¬
(*Q‘(*Q‘𝑥)) ∈ 𝐴) ↔ (𝑧 <Q
(*Q‘𝑥) ∧ ¬ 𝑥 ∈ 𝐴))) |
| 11 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
(*Q‘𝑥) ∈ V |
| 12 | | breq2 5147 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 =
(*Q‘𝑥) → (𝑧 <Q 𝑦 ↔ 𝑧 <Q
(*Q‘𝑥))) |
| 13 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 =
(*Q‘𝑥) →
(*Q‘𝑦) =
(*Q‘(*Q‘𝑥))) |
| 14 | 13 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 =
(*Q‘𝑥) →
((*Q‘𝑦) ∈ 𝐴 ↔
(*Q‘(*Q‘𝑥)) ∈ 𝐴)) |
| 15 | 14 | notbid 318 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 =
(*Q‘𝑥) → (¬
(*Q‘𝑦) ∈ 𝐴 ↔ ¬
(*Q‘(*Q‘𝑥)) ∈ 𝐴)) |
| 16 | 12, 15 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑦 =
(*Q‘𝑥) → ((𝑧 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) ↔ (𝑧 <Q
(*Q‘𝑥) ∧ ¬
(*Q‘(*Q‘𝑥)) ∈ 𝐴))) |
| 17 | 11, 16 | spcev 3606 |
. . . . . . . . . . . . 13
⊢ ((𝑧 <Q
(*Q‘𝑥) ∧ ¬
(*Q‘(*Q‘𝑥)) ∈ 𝐴) → ∃𝑦(𝑧 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴)) |
| 18 | 10, 17 | biimtrrdi 254 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ Q →
((𝑧
<Q (*Q‘𝑥) ∧ ¬ 𝑥 ∈ 𝐴) → ∃𝑦(𝑧 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴))) |
| 19 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
| 20 | | breq1 5146 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (𝑥 <Q 𝑦 ↔ 𝑧 <Q 𝑦)) |
| 21 | 20 | anbi1d 631 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → ((𝑥 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) ↔ (𝑧 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴))) |
| 22 | 21 | exbidv 1921 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (∃𝑦(𝑥 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) ↔ ∃𝑦(𝑧 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴))) |
| 23 | | reclempr.1 |
. . . . . . . . . . . . 13
⊢ 𝐵 = {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴)} |
| 24 | 19, 22, 23 | elab2 3682 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝐵 ↔ ∃𝑦(𝑧 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴)) |
| 25 | 18, 24 | imbitrrdi 252 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ Q →
((𝑧
<Q (*Q‘𝑥) ∧ ¬ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐵)) |
| 26 | 25 | expcomd 416 |
. . . . . . . . . 10
⊢ (𝑥 ∈ Q →
(¬ 𝑥 ∈ 𝐴 → (𝑧 <Q
(*Q‘𝑥) → 𝑧 ∈ 𝐵))) |
| 27 | 26 | imp 406 |
. . . . . . . . 9
⊢ ((𝑥 ∈ Q ∧
¬ 𝑥 ∈ 𝐴) → (𝑧 <Q
(*Q‘𝑥) → 𝑧 ∈ 𝐵)) |
| 28 | 27 | eximdv 1917 |
. . . . . . . 8
⊢ ((𝑥 ∈ Q ∧
¬ 𝑥 ∈ 𝐴) → (∃𝑧 𝑧 <Q
(*Q‘𝑥) → ∃𝑧 𝑧 ∈ 𝐵)) |
| 29 | 6, 28 | mpd 15 |
. . . . . . 7
⊢ ((𝑥 ∈ Q ∧
¬ 𝑥 ∈ 𝐴) → ∃𝑧 𝑧 ∈ 𝐵) |
| 30 | | n0 4353 |
. . . . . . 7
⊢ (𝐵 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝐵) |
| 31 | 29, 30 | sylibr 234 |
. . . . . 6
⊢ ((𝑥 ∈ Q ∧
¬ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅) |
| 32 | 31 | exlimiv 1930 |
. . . . 5
⊢
(∃𝑥(𝑥 ∈ Q ∧
¬ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅) |
| 33 | 1, 2, 32 | 3syl 18 |
. . . 4
⊢ (𝐴 ∈ P →
𝐵 ≠
∅) |
| 34 | | 0pss 4447 |
. . . 4
⊢ (∅
⊊ 𝐵 ↔ 𝐵 ≠ ∅) |
| 35 | 33, 34 | sylibr 234 |
. . 3
⊢ (𝐴 ∈ P →
∅ ⊊ 𝐵) |
| 36 | | prn0 11029 |
. . . . . 6
⊢ (𝐴 ∈ P →
𝐴 ≠
∅) |
| 37 | | elprnq 11031 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → 𝑧 ∈ Q) |
| 38 | | recrecnq 11007 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ Q →
(*Q‘(*Q‘𝑧)) = 𝑧) |
| 39 | 38 | eleq1d 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ Q →
((*Q‘(*Q‘𝑧)) ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
| 40 | 39 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ Q →
((𝐴 ∈ P
∧
(*Q‘(*Q‘𝑧)) ∈ 𝐴) ↔ (𝐴 ∈ P ∧ 𝑧 ∈ 𝐴))) |
| 41 | 37, 40 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → ((𝐴 ∈ P ∧
(*Q‘(*Q‘𝑧)) ∈ 𝐴) ↔ (𝐴 ∈ P ∧ 𝑧 ∈ 𝐴))) |
| 42 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢
(*Q‘𝑧) ∈ V |
| 43 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 =
(*Q‘𝑧) →
(*Q‘𝑥) =
(*Q‘(*Q‘𝑧))) |
| 44 | 43 | eleq1d 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑥 =
(*Q‘𝑧) →
((*Q‘𝑥) ∈ 𝐴 ↔
(*Q‘(*Q‘𝑧)) ∈ 𝐴)) |
| 45 | 44 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (𝑥 =
(*Q‘𝑧) → ((𝐴 ∈ P ∧
(*Q‘𝑥) ∈ 𝐴) ↔ (𝐴 ∈ P ∧
(*Q‘(*Q‘𝑧)) ∈ 𝐴))) |
| 46 | 42, 45 | spcev 3606 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
(*Q‘(*Q‘𝑧)) ∈ 𝐴) → ∃𝑥(𝐴 ∈ P ∧
(*Q‘𝑥) ∈ 𝐴)) |
| 47 | 41, 46 | biimtrrdi 254 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → ((𝐴 ∈ P ∧ 𝑧 ∈ 𝐴) → ∃𝑥(𝐴 ∈ P ∧
(*Q‘𝑥) ∈ 𝐴))) |
| 48 | 47 | pm2.43i 52 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → ∃𝑥(𝐴 ∈ P ∧
(*Q‘𝑥) ∈ 𝐴)) |
| 49 | | elprnq 11031 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
(*Q‘𝑥) ∈ 𝐴) →
(*Q‘𝑥) ∈ Q) |
| 50 | | dmrecnq 11008 |
. . . . . . . . . . . . . 14
⊢ dom
*Q = Q |
| 51 | | 0nnq 10964 |
. . . . . . . . . . . . . 14
⊢ ¬
∅ ∈ Q |
| 52 | 50, 51 | ndmfvrcl 6942 |
. . . . . . . . . . . . 13
⊢
((*Q‘𝑥) ∈ Q → 𝑥 ∈
Q) |
| 53 | 49, 52 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
(*Q‘𝑥) ∈ 𝐴) → 𝑥 ∈ Q) |
| 54 | | ltrnq 11019 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 <Q
𝑦 ↔
(*Q‘𝑦) <Q
(*Q‘𝑥)) |
| 55 | | prcdnq 11033 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ P ∧
(*Q‘𝑥) ∈ 𝐴) →
((*Q‘𝑦) <Q
(*Q‘𝑥) →
(*Q‘𝑦) ∈ 𝐴)) |
| 56 | 54, 55 | biimtrid 242 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ P ∧
(*Q‘𝑥) ∈ 𝐴) → (𝑥 <Q 𝑦 →
(*Q‘𝑦) ∈ 𝐴)) |
| 57 | 56 | alrimiv 1927 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
(*Q‘𝑥) ∈ 𝐴) → ∀𝑦(𝑥 <Q 𝑦 →
(*Q‘𝑦) ∈ 𝐴)) |
| 58 | 23 | eqabri 2885 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐵 ↔ ∃𝑦(𝑥 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴)) |
| 59 | | exanali 1859 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑦(𝑥 <Q
𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) ↔ ¬ ∀𝑦(𝑥 <Q 𝑦 →
(*Q‘𝑦) ∈ 𝐴)) |
| 60 | 58, 59 | bitri 275 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐵 ↔ ¬ ∀𝑦(𝑥 <Q 𝑦 →
(*Q‘𝑦) ∈ 𝐴)) |
| 61 | 60 | con2bii 357 |
. . . . . . . . . . . . 13
⊢
(∀𝑦(𝑥 <Q
𝑦 →
(*Q‘𝑦) ∈ 𝐴) ↔ ¬ 𝑥 ∈ 𝐵) |
| 62 | 57, 61 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
(*Q‘𝑥) ∈ 𝐴) → ¬ 𝑥 ∈ 𝐵) |
| 63 | 53, 62 | jca 511 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ P ∧
(*Q‘𝑥) ∈ 𝐴) → (𝑥 ∈ Q ∧ ¬ 𝑥 ∈ 𝐵)) |
| 64 | 63 | eximi 1835 |
. . . . . . . . . 10
⊢
(∃𝑥(𝐴 ∈ P ∧
(*Q‘𝑥) ∈ 𝐴) → ∃𝑥(𝑥 ∈ Q ∧ ¬ 𝑥 ∈ 𝐵)) |
| 65 | 48, 64 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → ∃𝑥(𝑥 ∈ Q ∧ ¬ 𝑥 ∈ 𝐵)) |
| 66 | 65 | ex 412 |
. . . . . . . 8
⊢ (𝐴 ∈ P →
(𝑧 ∈ 𝐴 → ∃𝑥(𝑥 ∈ Q ∧ ¬ 𝑥 ∈ 𝐵))) |
| 67 | 66 | exlimdv 1933 |
. . . . . . 7
⊢ (𝐴 ∈ P →
(∃𝑧 𝑧 ∈ 𝐴 → ∃𝑥(𝑥 ∈ Q ∧ ¬ 𝑥 ∈ 𝐵))) |
| 68 | | n0 4353 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝐴) |
| 69 | | nss 4048 |
. . . . . . 7
⊢ (¬
Q ⊆ 𝐵
↔ ∃𝑥(𝑥 ∈ Q ∧
¬ 𝑥 ∈ 𝐵)) |
| 70 | 67, 68, 69 | 3imtr4g 296 |
. . . . . 6
⊢ (𝐴 ∈ P →
(𝐴 ≠ ∅ →
¬ Q ⊆ 𝐵)) |
| 71 | 36, 70 | mpd 15 |
. . . . 5
⊢ (𝐴 ∈ P →
¬ Q ⊆ 𝐵) |
| 72 | | ltrelnq 10966 |
. . . . . . . . . . 11
⊢
<Q ⊆ (Q ×
Q) |
| 73 | 72 | brel 5750 |
. . . . . . . . . 10
⊢ (𝑥 <Q
𝑦 → (𝑥 ∈ Q ∧
𝑦 ∈
Q)) |
| 74 | 73 | simpld 494 |
. . . . . . . . 9
⊢ (𝑥 <Q
𝑦 → 𝑥 ∈ Q) |
| 75 | 74 | adantr 480 |
. . . . . . . 8
⊢ ((𝑥 <Q
𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → 𝑥 ∈ Q) |
| 76 | 75 | exlimiv 1930 |
. . . . . . 7
⊢
(∃𝑦(𝑥 <Q
𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → 𝑥 ∈ Q) |
| 77 | 58, 76 | sylbi 217 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵 → 𝑥 ∈ Q) |
| 78 | 77 | ssriv 3987 |
. . . . 5
⊢ 𝐵 ⊆
Q |
| 79 | 71, 78 | jctil 519 |
. . . 4
⊢ (𝐴 ∈ P →
(𝐵 ⊆ Q
∧ ¬ Q ⊆ 𝐵)) |
| 80 | | dfpss3 4089 |
. . . 4
⊢ (𝐵 ⊊ Q ↔
(𝐵 ⊆ Q
∧ ¬ Q ⊆ 𝐵)) |
| 81 | 79, 80 | sylibr 234 |
. . 3
⊢ (𝐴 ∈ P →
𝐵 ⊊
Q) |
| 82 | 35, 81 | jca 511 |
. 2
⊢ (𝐴 ∈ P →
(∅ ⊊ 𝐵 ∧
𝐵 ⊊
Q)) |
| 83 | | ltsonq 11009 |
. . . . . . . . . . 11
⊢
<Q Or Q |
| 84 | 83, 72 | sotri 6147 |
. . . . . . . . . 10
⊢ ((𝑧 <Q
𝑥 ∧ 𝑥 <Q 𝑦) → 𝑧 <Q 𝑦) |
| 85 | 84 | ex 412 |
. . . . . . . . 9
⊢ (𝑧 <Q
𝑥 → (𝑥 <Q
𝑦 → 𝑧 <Q 𝑦)) |
| 86 | 85 | anim1d 611 |
. . . . . . . 8
⊢ (𝑧 <Q
𝑥 → ((𝑥 <Q
𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → (𝑧 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴))) |
| 87 | 86 | eximdv 1917 |
. . . . . . 7
⊢ (𝑧 <Q
𝑥 → (∃𝑦(𝑥 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → ∃𝑦(𝑧 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴))) |
| 88 | 87, 58, 24 | 3imtr4g 296 |
. . . . . 6
⊢ (𝑧 <Q
𝑥 → (𝑥 ∈ 𝐵 → 𝑧 ∈ 𝐵)) |
| 89 | 88 | com12 32 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 → (𝑧 <Q 𝑥 → 𝑧 ∈ 𝐵)) |
| 90 | 89 | alrimiv 1927 |
. . . 4
⊢ (𝑥 ∈ 𝐵 → ∀𝑧(𝑧 <Q 𝑥 → 𝑧 ∈ 𝐵)) |
| 91 | | nfe1 2150 |
. . . . . . . . 9
⊢
Ⅎ𝑦∃𝑦(𝑥 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) |
| 92 | 91 | nfab 2911 |
. . . . . . . 8
⊢
Ⅎ𝑦{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴)} |
| 93 | 23, 92 | nfcxfr 2903 |
. . . . . . 7
⊢
Ⅎ𝑦𝐵 |
| 94 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑦 𝑥 <Q
𝑧 |
| 95 | 93, 94 | nfrexw 3313 |
. . . . . 6
⊢
Ⅎ𝑦∃𝑧 ∈ 𝐵 𝑥 <Q 𝑧 |
| 96 | | 19.8a 2181 |
. . . . . . . . . . . . 13
⊢ ((𝑧 <Q
𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → ∃𝑦(𝑧 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴)) |
| 97 | 96, 24 | sylibr 234 |
. . . . . . . . . . . 12
⊢ ((𝑧 <Q
𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → 𝑧 ∈ 𝐵) |
| 98 | 97 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝑥 <Q
𝑧 ∧ 𝑧 <Q 𝑦) ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → 𝑧 ∈ 𝐵) |
| 99 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝑥 <Q
𝑧 ∧ 𝑧 <Q 𝑦) ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → 𝑥 <Q 𝑧) |
| 100 | 98, 99 | jca 511 |
. . . . . . . . . 10
⊢ (((𝑥 <Q
𝑧 ∧ 𝑧 <Q 𝑦) ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → (𝑧 ∈ 𝐵 ∧ 𝑥 <Q 𝑧)) |
| 101 | 100 | expcom 413 |
. . . . . . . . 9
⊢ (¬
(*Q‘𝑦) ∈ 𝐴 → ((𝑥 <Q 𝑧 ∧ 𝑧 <Q 𝑦) → (𝑧 ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) |
| 102 | 101 | eximdv 1917 |
. . . . . . . 8
⊢ (¬
(*Q‘𝑦) ∈ 𝐴 → (∃𝑧(𝑥 <Q 𝑧 ∧ 𝑧 <Q 𝑦) → ∃𝑧(𝑧 ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) |
| 103 | | ltbtwnnq 11018 |
. . . . . . . 8
⊢ (𝑥 <Q
𝑦 ↔ ∃𝑧(𝑥 <Q 𝑧 ∧ 𝑧 <Q 𝑦)) |
| 104 | | df-rex 3071 |
. . . . . . . 8
⊢
(∃𝑧 ∈
𝐵 𝑥 <Q 𝑧 ↔ ∃𝑧(𝑧 ∈ 𝐵 ∧ 𝑥 <Q 𝑧)) |
| 105 | 102, 103,
104 | 3imtr4g 296 |
. . . . . . 7
⊢ (¬
(*Q‘𝑦) ∈ 𝐴 → (𝑥 <Q 𝑦 → ∃𝑧 ∈ 𝐵 𝑥 <Q 𝑧)) |
| 106 | 105 | impcom 407 |
. . . . . 6
⊢ ((𝑥 <Q
𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → ∃𝑧 ∈ 𝐵 𝑥 <Q 𝑧) |
| 107 | 95, 106 | exlimi 2217 |
. . . . 5
⊢
(∃𝑦(𝑥 <Q
𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → ∃𝑧 ∈ 𝐵 𝑥 <Q 𝑧) |
| 108 | 58, 107 | sylbi 217 |
. . . 4
⊢ (𝑥 ∈ 𝐵 → ∃𝑧 ∈ 𝐵 𝑥 <Q 𝑧) |
| 109 | 90, 108 | jca 511 |
. . 3
⊢ (𝑥 ∈ 𝐵 → (∀𝑧(𝑧 <Q 𝑥 → 𝑧 ∈ 𝐵) ∧ ∃𝑧 ∈ 𝐵 𝑥 <Q 𝑧)) |
| 110 | 109 | rgen 3063 |
. 2
⊢
∀𝑥 ∈
𝐵 (∀𝑧(𝑧 <Q 𝑥 → 𝑧 ∈ 𝐵) ∧ ∃𝑧 ∈ 𝐵 𝑥 <Q 𝑧) |
| 111 | | elnp 11027 |
. 2
⊢ (𝐵 ∈ P ↔
((∅ ⊊ 𝐵 ∧
𝐵 ⊊ Q)
∧ ∀𝑥 ∈
𝐵 (∀𝑧(𝑧 <Q 𝑥 → 𝑧 ∈ 𝐵) ∧ ∃𝑧 ∈ 𝐵 𝑥 <Q 𝑧))) |
| 112 | 82, 110, 111 | sylanblrc 590 |
1
⊢ (𝐴 ∈ P →
𝐵 ∈
P) |