Step | Hyp | Ref
| Expression |
1 | | ssid 3167 |
. . . . . 6
⊢
(2nd ‘1P) ⊆
(2nd ‘1P) |
2 | | rexss 3214 |
. . . . . 6
⊢
((2nd ‘1P) ⊆
(2nd ‘1P) → (∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ) ↔ ∃ℎ ∈ (2nd
‘1P)(ℎ ∈ (2nd
‘1P) ∧ 𝑥 = (𝑓 ·Q ℎ)))) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢
(∃ℎ ∈
(2nd ‘1P)𝑥 = (𝑓 ·Q ℎ) ↔ ∃ℎ ∈ (2nd
‘1P)(ℎ ∈ (2nd
‘1P) ∧ 𝑥 = (𝑓 ·Q ℎ))) |
4 | | 1pr 7503 |
. . . . . . . . . . 11
⊢
1P ∈ P |
5 | | prop 7424 |
. . . . . . . . . . . 12
⊢
(1P ∈ P →
〈(1st ‘1P), (2nd
‘1P)〉 ∈
P) |
6 | | elprnqu 7431 |
. . . . . . . . . . . 12
⊢
((〈(1st ‘1P),
(2nd ‘1P)〉 ∈
P ∧ ℎ
∈ (2nd ‘1P)) → ℎ ∈
Q) |
7 | 5, 6 | sylan 281 |
. . . . . . . . . . 11
⊢
((1P ∈ P ∧ ℎ ∈ (2nd
‘1P)) → ℎ ∈ Q) |
8 | 4, 7 | mpan 422 |
. . . . . . . . . 10
⊢ (ℎ ∈ (2nd
‘1P) → ℎ ∈ Q) |
9 | | prop 7424 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
10 | | elprnqu 7431 |
. . . . . . . . . . . 12
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑓 ∈ (2nd
‘𝐴)) → 𝑓 ∈
Q) |
11 | 9, 10 | sylan 281 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ (2nd
‘𝐴)) → 𝑓 ∈
Q) |
12 | | breq2 3991 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑓 ·Q ℎ) → (𝑓 <Q 𝑥 ↔ 𝑓 <Q (𝑓
·Q ℎ))) |
13 | 12 | 3ad2ant3 1015 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ Q ∧
ℎ ∈ Q
∧ 𝑥 = (𝑓
·Q ℎ)) → (𝑓 <Q 𝑥 ↔ 𝑓 <Q (𝑓
·Q ℎ))) |
14 | | 1pru 7505 |
. . . . . . . . . . . . . . 15
⊢
(2nd ‘1P) = {ℎ ∣
1Q <Q ℎ} |
15 | 14 | abeq2i 2281 |
. . . . . . . . . . . . . 14
⊢ (ℎ ∈ (2nd
‘1P) ↔ 1Q
<Q ℎ) |
16 | | 1nq 7315 |
. . . . . . . . . . . . . . . . 17
⊢
1Q ∈ Q |
17 | | ltmnqg 7350 |
. . . . . . . . . . . . . . . . 17
⊢
((1Q ∈ Q ∧ ℎ ∈ Q ∧
𝑓 ∈ Q)
→ (1Q <Q ℎ ↔ (𝑓 ·Q
1Q) <Q (𝑓 ·Q ℎ))) |
18 | 16, 17 | mp3an1 1319 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ ∈ Q ∧
𝑓 ∈ Q)
→ (1Q <Q ℎ ↔ (𝑓 ·Q
1Q) <Q (𝑓 ·Q ℎ))) |
19 | 18 | ancoms 266 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ Q ∧
ℎ ∈ Q)
→ (1Q <Q ℎ ↔ (𝑓 ·Q
1Q) <Q (𝑓 ·Q ℎ))) |
20 | | mulidnq 7338 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ Q →
(𝑓
·Q 1Q) = 𝑓) |
21 | 20 | breq1d 3997 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ Q →
((𝑓
·Q 1Q)
<Q (𝑓 ·Q ℎ) ↔ 𝑓 <Q (𝑓
·Q ℎ))) |
22 | 21 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ Q ∧
ℎ ∈ Q)
→ ((𝑓
·Q 1Q)
<Q (𝑓 ·Q ℎ) ↔ 𝑓 <Q (𝑓
·Q ℎ))) |
23 | 19, 22 | bitrd 187 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ Q ∧
ℎ ∈ Q)
→ (1Q <Q ℎ ↔ 𝑓 <Q (𝑓
·Q ℎ))) |
24 | 15, 23 | bitr2id 192 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ Q ∧
ℎ ∈ Q)
→ (𝑓
<Q (𝑓 ·Q ℎ) ↔ ℎ ∈ (2nd
‘1P))) |
25 | 24 | 3adant3 1012 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ Q ∧
ℎ ∈ Q
∧ 𝑥 = (𝑓
·Q ℎ)) → (𝑓 <Q (𝑓
·Q ℎ) ↔ ℎ ∈ (2nd
‘1P))) |
26 | 13, 25 | bitrd 187 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ Q ∧
ℎ ∈ Q
∧ 𝑥 = (𝑓
·Q ℎ)) → (𝑓 <Q 𝑥 ↔ ℎ ∈ (2nd
‘1P))) |
27 | 11, 26 | syl3an1 1266 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ P ∧
𝑓 ∈ (2nd
‘𝐴)) ∧ ℎ ∈ Q ∧
𝑥 = (𝑓 ·Q ℎ)) → (𝑓 <Q 𝑥 ↔ ℎ ∈ (2nd
‘1P))) |
28 | 8, 27 | syl3an2 1267 |
. . . . . . . . 9
⊢ (((𝐴 ∈ P ∧
𝑓 ∈ (2nd
‘𝐴)) ∧ ℎ ∈ (2nd
‘1P) ∧ 𝑥 = (𝑓 ·Q ℎ)) → (𝑓 <Q 𝑥 ↔ ℎ ∈ (2nd
‘1P))) |
29 | 28 | 3expia 1200 |
. . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝑓 ∈ (2nd
‘𝐴)) ∧ ℎ ∈ (2nd
‘1P)) → (𝑥 = (𝑓 ·Q ℎ) → (𝑓 <Q 𝑥 ↔ ℎ ∈ (2nd
‘1P)))) |
30 | 29 | pm5.32rd 448 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝑓 ∈ (2nd
‘𝐴)) ∧ ℎ ∈ (2nd
‘1P)) → ((𝑓 <Q 𝑥 ∧ 𝑥 = (𝑓 ·Q ℎ)) ↔ (ℎ ∈ (2nd
‘1P) ∧ 𝑥 = (𝑓 ·Q ℎ)))) |
31 | 30 | rexbidva 2467 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ (2nd
‘𝐴)) →
(∃ℎ ∈
(2nd ‘1P)(𝑓 <Q 𝑥 ∧ 𝑥 = (𝑓 ·Q ℎ)) ↔ ∃ℎ ∈ (2nd
‘1P)(ℎ ∈ (2nd
‘1P) ∧ 𝑥 = (𝑓 ·Q ℎ)))) |
32 | | r19.42v 2627 |
. . . . . 6
⊢
(∃ℎ ∈
(2nd ‘1P)(𝑓 <Q 𝑥 ∧ 𝑥 = (𝑓 ·Q ℎ)) ↔ (𝑓 <Q 𝑥 ∧ ∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ))) |
33 | 31, 32 | bitr3di 194 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ (2nd
‘𝐴)) →
(∃ℎ ∈
(2nd ‘1P)(ℎ ∈ (2nd
‘1P) ∧ 𝑥 = (𝑓 ·Q ℎ)) ↔ (𝑓 <Q 𝑥 ∧ ∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ)))) |
34 | 3, 33 | syl5bb 191 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ (2nd
‘𝐴)) →
(∃ℎ ∈
(2nd ‘1P)𝑥 = (𝑓 ·Q ℎ) ↔ (𝑓 <Q 𝑥 ∧ ∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ)))) |
35 | 34 | rexbidva 2467 |
. . 3
⊢ (𝐴 ∈ P →
(∃𝑓 ∈
(2nd ‘𝐴)∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ) ↔ ∃𝑓 ∈ (2nd
‘𝐴)(𝑓 <Q
𝑥 ∧ ∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ)))) |
36 | | df-imp 7418 |
. . . . 5
⊢
·P = (𝑦 ∈ P, 𝑧 ∈ P ↦ 〈{𝑤 ∈ Q ∣
∃𝑢 ∈
Q ∃𝑣
∈ Q (𝑢
∈ (1st ‘𝑦) ∧ 𝑣 ∈ (1st ‘𝑧) ∧ 𝑤 = (𝑢 ·Q 𝑣))}, {𝑤 ∈ Q ∣ ∃𝑢 ∈ Q
∃𝑣 ∈
Q (𝑢 ∈
(2nd ‘𝑦)
∧ 𝑣 ∈
(2nd ‘𝑧)
∧ 𝑤 = (𝑢
·Q 𝑣))}〉) |
37 | | mulclnq 7325 |
. . . . 5
⊢ ((𝑢 ∈ Q ∧
𝑣 ∈ Q)
→ (𝑢
·Q 𝑣) ∈ Q) |
38 | 36, 37 | genpelvu 7462 |
. . . 4
⊢ ((𝐴 ∈ P ∧
1P ∈ P) → (𝑥 ∈ (2nd ‘(𝐴
·P 1P)) ↔
∃𝑓 ∈
(2nd ‘𝐴)∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ))) |
39 | 4, 38 | mpan2 423 |
. . 3
⊢ (𝐴 ∈ P →
(𝑥 ∈ (2nd
‘(𝐴
·P 1P)) ↔
∃𝑓 ∈
(2nd ‘𝐴)∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ))) |
40 | | prnminu 7438 |
. . . . . . 7
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑥 ∈ (2nd
‘𝐴)) →
∃𝑓 ∈
(2nd ‘𝐴)𝑓 <Q 𝑥) |
41 | 9, 40 | sylan 281 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑥 ∈ (2nd
‘𝐴)) →
∃𝑓 ∈
(2nd ‘𝐴)𝑓 <Q 𝑥) |
42 | | ltrelnq 7314 |
. . . . . . . . . . . . . 14
⊢
<Q ⊆ (Q ×
Q) |
43 | 42 | brel 4661 |
. . . . . . . . . . . . 13
⊢ (𝑓 <Q
𝑥 → (𝑓 ∈ Q ∧
𝑥 ∈
Q)) |
44 | 43 | ancomd 265 |
. . . . . . . . . . . 12
⊢ (𝑓 <Q
𝑥 → (𝑥 ∈ Q ∧
𝑓 ∈
Q)) |
45 | | ltmnqg 7350 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q
∧ 𝑤 ∈
Q) → (𝑦
<Q 𝑧 ↔ (𝑤 ·Q 𝑦) <Q
(𝑤
·Q 𝑧))) |
46 | 45 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ Q ∧
𝑓 ∈ Q)
∧ (𝑦 ∈
Q ∧ 𝑧
∈ Q ∧ 𝑤 ∈ Q)) → (𝑦 <Q
𝑧 ↔ (𝑤
·Q 𝑦) <Q (𝑤
·Q 𝑧))) |
47 | | simpr 109 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ 𝑓 ∈
Q) |
48 | | simpl 108 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ 𝑥 ∈
Q) |
49 | | recclnq 7341 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ Q →
(*Q‘𝑓) ∈ Q) |
50 | 49 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ (*Q‘𝑓) ∈ Q) |
51 | | mulcomnqg 7332 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦
·Q 𝑧) = (𝑧 ·Q 𝑦)) |
52 | 51 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ Q ∧
𝑓 ∈ Q)
∧ (𝑦 ∈
Q ∧ 𝑧
∈ Q)) → (𝑦 ·Q 𝑧) = (𝑧 ·Q 𝑦)) |
53 | 46, 47, 48, 50, 52 | caovord2d 6019 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ (𝑓
<Q 𝑥 ↔ (𝑓 ·Q
(*Q‘𝑓)) <Q (𝑥
·Q (*Q‘𝑓)))) |
54 | | recidnq 7342 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ Q →
(𝑓
·Q (*Q‘𝑓)) =
1Q) |
55 | 54 | breq1d 3997 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ Q →
((𝑓
·Q (*Q‘𝑓))
<Q (𝑥 ·Q
(*Q‘𝑓)) ↔ 1Q
<Q (𝑥 ·Q
(*Q‘𝑓)))) |
56 | 55 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ ((𝑓
·Q (*Q‘𝑓))
<Q (𝑥 ·Q
(*Q‘𝑓)) ↔ 1Q
<Q (𝑥 ·Q
(*Q‘𝑓)))) |
57 | 53, 56 | bitrd 187 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ (𝑓
<Q 𝑥 ↔ 1Q
<Q (𝑥 ·Q
(*Q‘𝑓)))) |
58 | 57 | biimpd 143 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ (𝑓
<Q 𝑥 → 1Q
<Q (𝑥 ·Q
(*Q‘𝑓)))) |
59 | 44, 58 | mpcom 36 |
. . . . . . . . . . 11
⊢ (𝑓 <Q
𝑥 →
1Q <Q (𝑥 ·Q
(*Q‘𝑓))) |
60 | | mulclnq 7325 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ Q ∧
(*Q‘𝑓) ∈ Q) → (𝑥
·Q (*Q‘𝑓)) ∈
Q) |
61 | 49, 60 | sylan2 284 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ (𝑥
·Q (*Q‘𝑓)) ∈
Q) |
62 | | breq2 3991 |
. . . . . . . . . . . . 13
⊢ (ℎ = (𝑥 ·Q
(*Q‘𝑓)) → (1Q
<Q ℎ ↔ 1Q
<Q (𝑥 ·Q
(*Q‘𝑓)))) |
63 | 62, 14 | elab2g 2877 |
. . . . . . . . . . . 12
⊢ ((𝑥
·Q (*Q‘𝑓)) ∈ Q →
((𝑥
·Q (*Q‘𝑓)) ∈ (2nd
‘1P) ↔ 1Q
<Q (𝑥 ·Q
(*Q‘𝑓)))) |
64 | 44, 61, 63 | 3syl 17 |
. . . . . . . . . . 11
⊢ (𝑓 <Q
𝑥 → ((𝑥
·Q (*Q‘𝑓)) ∈ (2nd
‘1P) ↔ 1Q
<Q (𝑥 ·Q
(*Q‘𝑓)))) |
65 | 59, 64 | mpbird 166 |
. . . . . . . . . 10
⊢ (𝑓 <Q
𝑥 → (𝑥
·Q (*Q‘𝑓)) ∈ (2nd
‘1P)) |
66 | | mulassnqg 7333 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q
∧ 𝑤 ∈
Q) → ((𝑦
·Q 𝑧) ·Q 𝑤) = (𝑦 ·Q (𝑧
·Q 𝑤))) |
67 | 66 | adantl 275 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ Q ∧
𝑓 ∈ Q)
∧ (𝑦 ∈
Q ∧ 𝑧
∈ Q ∧ 𝑤 ∈ Q)) → ((𝑦
·Q 𝑧) ·Q 𝑤) = (𝑦 ·Q (𝑧
·Q 𝑤))) |
68 | 47, 48, 50, 52, 67 | caov12d 6031 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ (𝑓
·Q (𝑥 ·Q
(*Q‘𝑓))) = (𝑥 ·Q (𝑓
·Q (*Q‘𝑓)))) |
69 | 54 | oveq2d 5866 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ Q →
(𝑥
·Q (𝑓 ·Q
(*Q‘𝑓))) = (𝑥 ·Q
1Q)) |
70 | 69 | adantl 275 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ (𝑥
·Q (𝑓 ·Q
(*Q‘𝑓))) = (𝑥 ·Q
1Q)) |
71 | | mulidnq 7338 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ Q →
(𝑥
·Q 1Q) = 𝑥) |
72 | 71 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ (𝑥
·Q 1Q) = 𝑥) |
73 | 68, 70, 72 | 3eqtrrd 2208 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ 𝑥 = (𝑓
·Q (𝑥 ·Q
(*Q‘𝑓)))) |
74 | 44, 73 | syl 14 |
. . . . . . . . . 10
⊢ (𝑓 <Q
𝑥 → 𝑥 = (𝑓 ·Q (𝑥
·Q (*Q‘𝑓)))) |
75 | | oveq2 5858 |
. . . . . . . . . . . 12
⊢ (ℎ = (𝑥 ·Q
(*Q‘𝑓)) → (𝑓 ·Q ℎ) = (𝑓 ·Q (𝑥
·Q (*Q‘𝑓)))) |
76 | 75 | eqeq2d 2182 |
. . . . . . . . . . 11
⊢ (ℎ = (𝑥 ·Q
(*Q‘𝑓)) → (𝑥 = (𝑓 ·Q ℎ) ↔ 𝑥 = (𝑓 ·Q (𝑥
·Q (*Q‘𝑓))))) |
77 | 76 | rspcev 2834 |
. . . . . . . . . 10
⊢ (((𝑥
·Q (*Q‘𝑓)) ∈ (2nd
‘1P) ∧ 𝑥 = (𝑓 ·Q (𝑥
·Q (*Q‘𝑓)))) → ∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ)) |
78 | 65, 74, 77 | syl2anc 409 |
. . . . . . . . 9
⊢ (𝑓 <Q
𝑥 → ∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ)) |
79 | 78 | a1i 9 |
. . . . . . . 8
⊢ (𝑓 ∈ (2nd
‘𝐴) → (𝑓 <Q
𝑥 → ∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ))) |
80 | 79 | ancld 323 |
. . . . . . 7
⊢ (𝑓 ∈ (2nd
‘𝐴) → (𝑓 <Q
𝑥 → (𝑓 <Q
𝑥 ∧ ∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ)))) |
81 | 80 | reximia 2565 |
. . . . . 6
⊢
(∃𝑓 ∈
(2nd ‘𝐴)𝑓 <Q 𝑥 → ∃𝑓 ∈ (2nd
‘𝐴)(𝑓 <Q
𝑥 ∧ ∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ))) |
82 | 41, 81 | syl 14 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑥 ∈ (2nd
‘𝐴)) →
∃𝑓 ∈
(2nd ‘𝐴)(𝑓 <Q 𝑥 ∧ ∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ))) |
83 | 82 | ex 114 |
. . . 4
⊢ (𝐴 ∈ P →
(𝑥 ∈ (2nd
‘𝐴) →
∃𝑓 ∈
(2nd ‘𝐴)(𝑓 <Q 𝑥 ∧ ∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ)))) |
84 | | prcunqu 7434 |
. . . . . . 7
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑓 ∈ (2nd
‘𝐴)) → (𝑓 <Q
𝑥 → 𝑥 ∈ (2nd ‘𝐴))) |
85 | 9, 84 | sylan 281 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ (2nd
‘𝐴)) → (𝑓 <Q
𝑥 → 𝑥 ∈ (2nd ‘𝐴))) |
86 | 85 | adantrd 277 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ (2nd
‘𝐴)) → ((𝑓 <Q
𝑥 ∧ ∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ)) → 𝑥 ∈ (2nd ‘𝐴))) |
87 | 86 | rexlimdva 2587 |
. . . 4
⊢ (𝐴 ∈ P →
(∃𝑓 ∈
(2nd ‘𝐴)(𝑓 <Q 𝑥 ∧ ∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ)) → 𝑥 ∈ (2nd ‘𝐴))) |
88 | 83, 87 | impbid 128 |
. . 3
⊢ (𝐴 ∈ P →
(𝑥 ∈ (2nd
‘𝐴) ↔
∃𝑓 ∈
(2nd ‘𝐴)(𝑓 <Q 𝑥 ∧ ∃ℎ ∈ (2nd
‘1P)𝑥 = (𝑓 ·Q ℎ)))) |
89 | 35, 39, 88 | 3bitr4d 219 |
. 2
⊢ (𝐴 ∈ P →
(𝑥 ∈ (2nd
‘(𝐴
·P 1P)) ↔ 𝑥 ∈ (2nd
‘𝐴))) |
90 | 89 | eqrdv 2168 |
1
⊢ (𝐴 ∈ P →
(2nd ‘(𝐴
·P 1P)) =
(2nd ‘𝐴)) |