Step | Hyp | Ref
| Expression |
1 | | prop 7437 |
. . 3
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
2 | | prmu 7440 |
. . 3
⊢
(〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P →
∃𝑧 ∈
Q 𝑧 ∈
(2nd ‘𝐴)) |
3 | 1, 2 | syl 14 |
. 2
⊢ (𝐴 ∈ P →
∃𝑧 ∈
Q 𝑧 ∈
(2nd ‘𝐴)) |
4 | | archnqq 7379 |
. . . 4
⊢ (𝑧 ∈ Q →
∃𝑥 ∈
N 𝑧
<Q [〈𝑥, 1o〉]
~Q ) |
5 | 4 | ad2antrl 487 |
. . 3
⊢ ((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
→ ∃𝑥 ∈
N 𝑧
<Q [〈𝑥, 1o〉]
~Q ) |
6 | | simprl 526 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
→ 𝑧 ∈
Q) |
7 | 6 | ad2antrr 485 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [〈𝑥, 1o〉]
~Q ) → 𝑧 ∈ Q) |
8 | | simprr 527 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
→ 𝑧 ∈
(2nd ‘𝐴)) |
9 | 8 | ad2antrr 485 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [〈𝑥, 1o〉]
~Q ) → 𝑧 ∈ (2nd ‘𝐴)) |
10 | | simpr 109 |
. . . . . . . 8
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [〈𝑥, 1o〉]
~Q ) → 𝑧 <Q [〈𝑥, 1o〉]
~Q ) |
11 | | vex 2733 |
. . . . . . . . 9
⊢ 𝑧 ∈ V |
12 | | breq1 3992 |
. . . . . . . . 9
⊢ (𝑙 = 𝑧 → (𝑙 <Q [〈𝑥, 1o〉]
~Q ↔ 𝑧 <Q [〈𝑥, 1o〉]
~Q )) |
13 | | ltnqex 7511 |
. . . . . . . . . 10
⊢ {𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q } ∈ V |
14 | | gtnqex 7512 |
. . . . . . . . . 10
⊢ {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢} ∈ V |
15 | 13, 14 | op1st 6125 |
. . . . . . . . 9
⊢
(1st ‘〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉) = {𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q } |
16 | 11, 12, 15 | elab2 2878 |
. . . . . . . 8
⊢ (𝑧 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉) ↔ 𝑧 <Q [〈𝑥, 1o〉]
~Q ) |
17 | 10, 16 | sylibr 133 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [〈𝑥, 1o〉]
~Q ) → 𝑧 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉)) |
18 | | eleq1 2233 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (𝑤 ∈ (2nd ‘𝐴) ↔ 𝑧 ∈ (2nd ‘𝐴))) |
19 | | eleq1 2233 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (𝑤 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉) ↔ 𝑧 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉))) |
20 | 18, 19 | anbi12d 470 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → ((𝑤 ∈ (2nd ‘𝐴) ∧ 𝑤 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉)) ↔ (𝑧 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉)))) |
21 | 20 | rspcev 2834 |
. . . . . . 7
⊢ ((𝑧 ∈ Q ∧
(𝑧 ∈ (2nd
‘𝐴) ∧ 𝑧 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉))) → ∃𝑤 ∈ Q (𝑤 ∈ (2nd ‘𝐴) ∧ 𝑤 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉))) |
22 | 7, 9, 17, 21 | syl12anc 1231 |
. . . . . 6
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [〈𝑥, 1o〉]
~Q ) → ∃𝑤 ∈ Q (𝑤 ∈ (2nd ‘𝐴) ∧ 𝑤 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉))) |
23 | | simplll 528 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [〈𝑥, 1o〉]
~Q ) → 𝐴 ∈ P) |
24 | | nnprlu 7515 |
. . . . . . . 8
⊢ (𝑥 ∈ N →
〈{𝑙 ∣ 𝑙 <Q
[〈𝑥,
1o〉] ~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉 ∈
P) |
25 | 24 | ad2antlr 486 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [〈𝑥, 1o〉]
~Q ) → 〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉 ∈
P) |
26 | | ltdfpr 7468 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
〈{𝑙 ∣ 𝑙 <Q
[〈𝑥,
1o〉] ~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉 ∈ P) → (𝐴<P
〈{𝑙 ∣ 𝑙 <Q
[〈𝑥,
1o〉] ~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉 ↔ ∃𝑤 ∈ Q (𝑤 ∈ (2nd ‘𝐴) ∧ 𝑤 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉)))) |
27 | 23, 25, 26 | syl2anc 409 |
. . . . . 6
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [〈𝑥, 1o〉]
~Q ) → (𝐴<P 〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉 ↔ ∃𝑤 ∈ Q (𝑤 ∈ (2nd ‘𝐴) ∧ 𝑤 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉)))) |
28 | 22, 27 | mpbird 166 |
. . . . 5
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [〈𝑥, 1o〉]
~Q ) → 𝐴<P 〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉) |
29 | 28 | ex 114 |
. . . 4
⊢ (((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) → (𝑧
<Q [〈𝑥, 1o〉]
~Q → 𝐴<P 〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉)) |
30 | 29 | reximdva 2572 |
. . 3
⊢ ((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
→ (∃𝑥 ∈
N 𝑧
<Q [〈𝑥, 1o〉]
~Q → ∃𝑥 ∈ N 𝐴<P 〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉)) |
31 | 5, 30 | mpd 13 |
. 2
⊢ ((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
→ ∃𝑥 ∈
N 𝐴<P 〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉) |
32 | 3, 31 | rexlimddv 2592 |
1
⊢ (𝐴 ∈ P →
∃𝑥 ∈
N 𝐴<P 〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉]
~Q }, {𝑢 ∣ [〈𝑥, 1o〉]
~Q <Q 𝑢}〉) |