Step | Hyp | Ref
| Expression |
1 | | prop 7474 |
. . 3
⊢ (𝐴 ∈ P →
⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈
P) |
2 | | prmu 7477 |
. . 3
⊢
(⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ P →
∃𝑧 ∈
Q 𝑧 ∈
(2nd ‘𝐴)) |
3 | 1, 2 | syl 14 |
. 2
⊢ (𝐴 ∈ P →
∃𝑧 ∈
Q 𝑧 ∈
(2nd ‘𝐴)) |
4 | | archnqq 7416 |
. . . 4
⊢ (𝑧 ∈ Q →
∃𝑥 ∈
N 𝑧
<Q [⟨𝑥, 1o⟩]
~Q ) |
5 | 4 | ad2antrl 490 |
. . 3
⊢ ((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
→ ∃𝑥 ∈
N 𝑧
<Q [⟨𝑥, 1o⟩]
~Q ) |
6 | | simprl 529 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
→ 𝑧 ∈
Q) |
7 | 6 | ad2antrr 488 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [⟨𝑥, 1o⟩]
~Q ) → 𝑧 ∈ Q) |
8 | | simprr 531 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
→ 𝑧 ∈
(2nd ‘𝐴)) |
9 | 8 | ad2antrr 488 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [⟨𝑥, 1o⟩]
~Q ) → 𝑧 ∈ (2nd ‘𝐴)) |
10 | | simpr 110 |
. . . . . . . 8
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [⟨𝑥, 1o⟩]
~Q ) → 𝑧 <Q [⟨𝑥, 1o⟩]
~Q ) |
11 | | vex 2741 |
. . . . . . . . 9
⊢ 𝑧 ∈ V |
12 | | breq1 4007 |
. . . . . . . . 9
⊢ (𝑙 = 𝑧 → (𝑙 <Q [⟨𝑥, 1o⟩]
~Q ↔ 𝑧 <Q [⟨𝑥, 1o⟩]
~Q )) |
13 | | ltnqex 7548 |
. . . . . . . . . 10
⊢ {𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩]
~Q } ∈ V |
14 | | gtnqex 7549 |
. . . . . . . . . 10
⊢ {𝑢 ∣ [⟨𝑥, 1o⟩]
~Q <Q 𝑢} ∈ V |
15 | 13, 14 | op1st 6147 |
. . . . . . . . 9
⊢
(1st ‘⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩]
~Q <Q 𝑢}⟩) = {𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩]
~Q } |
16 | 11, 12, 15 | elab2 2886 |
. . . . . . . 8
⊢ (𝑧 ∈ (1st
‘⟨{𝑙 ∣
𝑙
<Q [⟨𝑥, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩]
~Q <Q 𝑢}⟩) ↔ 𝑧 <Q [⟨𝑥, 1o⟩]
~Q ) |
17 | 10, 16 | sylibr 134 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [⟨𝑥, 1o⟩]
~Q ) → 𝑧 ∈ (1st ‘⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩]
~Q <Q 𝑢}⟩)) |
18 | | eleq1 2240 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (𝑤 ∈ (2nd ‘𝐴) ↔ 𝑧 ∈ (2nd ‘𝐴))) |
19 | | eleq1 2240 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (𝑤 ∈ (1st ‘⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩]
~Q <Q 𝑢}⟩) ↔ 𝑧 ∈ (1st ‘⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩]
~Q <Q 𝑢}⟩))) |
20 | 18, 19 | anbi12d 473 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → ((𝑤 ∈ (2nd ‘𝐴) ∧ 𝑤 ∈ (1st ‘⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩]
~Q <Q 𝑢}⟩)) ↔ (𝑧 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (1st ‘⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩]
~Q <Q 𝑢}⟩)))) |
21 | 20 | rspcev 2842 |
. . . . . . 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 1236 |
. . . . . 6
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [⟨𝑥, 1o⟩]
~Q ) → ∃𝑤 ∈ Q (𝑤 ∈ (2nd ‘𝐴) ∧ 𝑤 ∈ (1st ‘⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩]
~Q <Q 𝑢}⟩))) |
23 | | simplll 533 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [⟨𝑥, 1o⟩]
~Q ) → 𝐴 ∈ P) |
24 | | nnprlu 7552 |
. . . . . . . 8
⊢ (𝑥 ∈ N →
⟨{𝑙 ∣ 𝑙 <Q
[⟨𝑥,
1o⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩]
~Q <Q 𝑢}⟩ ∈
P) |
25 | 24 | ad2antlr 489 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [⟨𝑥, 1o⟩]
~Q ) → ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩]
~Q <Q 𝑢}⟩ ∈
P) |
26 | | ltdfpr 7505 |
. . . . . . 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 411 |
. . . . . 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 167 |
. . . . 5
⊢ ((((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) ∧ 𝑧
<Q [⟨𝑥, 1o⟩]
~Q ) → 𝐴<P ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩]
~Q <Q 𝑢}⟩) |
29 | 28 | ex 115 |
. . . 4
⊢ (((𝐴 ∈ P ∧
(𝑧 ∈ Q
∧ 𝑧 ∈
(2nd ‘𝐴)))
∧ 𝑥 ∈
N) → (𝑧
<Q [⟨𝑥, 1o⟩]
~Q → 𝐴<P ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩]
~Q <Q 𝑢}⟩)) |
30 | 29 | reximdva 2579 |
. . 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 2599 |
1
⊢ (𝐴 ∈ P →
∃𝑥 ∈
N 𝐴<P ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩]
~Q <Q 𝑢}⟩) |