Proof of Theorem genpelxp
Step | Hyp | Ref
| Expression |
1 | | ssrab2 3232 |
. . . . 5
⊢ {𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝐴) ∧ 𝑧 ∈ (1st ‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧))} ⊆ Q |
2 | | nqex 7318 |
. . . . . 6
⊢
Q ∈ V |
3 | 2 | elpw2 4141 |
. . . . 5
⊢ ({𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝐴) ∧ 𝑧 ∈ (1st ‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧))} ∈ 𝒫 Q ↔
{𝑥 ∈ Q
∣ ∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝐴) ∧ 𝑧 ∈ (1st ‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧))} ⊆ Q) |
4 | 1, 3 | mpbir 145 |
. . . 4
⊢ {𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝐴) ∧ 𝑧 ∈ (1st ‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧))} ∈ 𝒫
Q |
5 | | ssrab2 3232 |
. . . . 5
⊢ {𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧))} ⊆ Q |
6 | 2 | elpw2 4141 |
. . . . 5
⊢ ({𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧))} ∈ 𝒫 Q ↔
{𝑥 ∈ Q
∣ ∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧))} ⊆ Q) |
7 | 5, 6 | mpbir 145 |
. . . 4
⊢ {𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧))} ∈ 𝒫
Q |
8 | | opelxpi 4641 |
. . . 4
⊢ (({𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝐴) ∧ 𝑧 ∈ (1st ‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧))} ∈ 𝒫 Q ∧
{𝑥 ∈ Q
∣ ∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧))} ∈ 𝒫 Q) →
〈{𝑥 ∈
Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st
‘𝐴) ∧ 𝑧 ∈ (1st
‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ 𝑧 ∈
(2nd ‘𝐵)
∧ 𝑥 = (𝑦𝐺𝑧))}〉 ∈ (𝒫 Q
× 𝒫 Q)) |
9 | 4, 7, 8 | mp2an 424 |
. . 3
⊢
〈{𝑥 ∈
Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st
‘𝐴) ∧ 𝑧 ∈ (1st
‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ 𝑧 ∈
(2nd ‘𝐵)
∧ 𝑥 = (𝑦𝐺𝑧))}〉 ∈ (𝒫 Q
× 𝒫 Q) |
10 | | fveq2 5494 |
. . . . . . . . 9
⊢ (𝑤 = 𝐴 → (1st ‘𝑤) = (1st ‘𝐴)) |
11 | 10 | eleq2d 2240 |
. . . . . . . 8
⊢ (𝑤 = 𝐴 → (𝑦 ∈ (1st ‘𝑤) ↔ 𝑦 ∈ (1st ‘𝐴))) |
12 | 11 | 3anbi1d 1311 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → ((𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧)) ↔ (𝑦 ∈ (1st ‘𝐴) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧)))) |
13 | 12 | 2rexbidv 2495 |
. . . . . 6
⊢ (𝑤 = 𝐴 → (∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st
‘𝑤) ∧ 𝑧 ∈ (1st
‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧)) ↔ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st
‘𝐴) ∧ 𝑧 ∈ (1st
‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧)))) |
14 | 13 | rabbidv 2719 |
. . . . 5
⊢ (𝑤 = 𝐴 → {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(1st ‘𝑤)
∧ 𝑧 ∈
(1st ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))} = {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(1st ‘𝐴)
∧ 𝑧 ∈
(1st ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}) |
15 | | fveq2 5494 |
. . . . . . . . 9
⊢ (𝑤 = 𝐴 → (2nd ‘𝑤) = (2nd ‘𝐴)) |
16 | 15 | eleq2d 2240 |
. . . . . . . 8
⊢ (𝑤 = 𝐴 → (𝑦 ∈ (2nd ‘𝑤) ↔ 𝑦 ∈ (2nd ‘𝐴))) |
17 | 16 | 3anbi1d 1311 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → ((𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧)) ↔ (𝑦 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧)))) |
18 | 17 | 2rexbidv 2495 |
. . . . . 6
⊢ (𝑤 = 𝐴 → (∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd
‘𝑤) ∧ 𝑧 ∈ (2nd
‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧)) ↔ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd
‘𝐴) ∧ 𝑧 ∈ (2nd
‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧)))) |
19 | 18 | rabbidv 2719 |
. . . . 5
⊢ (𝑤 = 𝐴 → {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))} = {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}) |
20 | 14, 19 | opeq12d 3771 |
. . . 4
⊢ (𝑤 = 𝐴 → 〈{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(1st ‘𝑤)
∧ 𝑧 ∈
(1st ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉 = 〈{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(1st ‘𝐴)
∧ 𝑧 ∈
(1st ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) |
21 | | fveq2 5494 |
. . . . . . . . 9
⊢ (𝑣 = 𝐵 → (1st ‘𝑣) = (1st ‘𝐵)) |
22 | 21 | eleq2d 2240 |
. . . . . . . 8
⊢ (𝑣 = 𝐵 → (𝑧 ∈ (1st ‘𝑣) ↔ 𝑧 ∈ (1st ‘𝐵))) |
23 | 22 | 3anbi2d 1312 |
. . . . . . 7
⊢ (𝑣 = 𝐵 → ((𝑦 ∈ (1st ‘𝐴) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧)) ↔ (𝑦 ∈ (1st ‘𝐴) ∧ 𝑧 ∈ (1st ‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧)))) |
24 | 23 | 2rexbidv 2495 |
. . . . . 6
⊢ (𝑣 = 𝐵 → (∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st
‘𝐴) ∧ 𝑧 ∈ (1st
‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧)) ↔ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st
‘𝐴) ∧ 𝑧 ∈ (1st
‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧)))) |
25 | 24 | rabbidv 2719 |
. . . . 5
⊢ (𝑣 = 𝐵 → {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(1st ‘𝐴)
∧ 𝑧 ∈
(1st ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))} = {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(1st ‘𝐴)
∧ 𝑧 ∈
(1st ‘𝐵)
∧ 𝑥 = (𝑦𝐺𝑧))}) |
26 | | fveq2 5494 |
. . . . . . . . 9
⊢ (𝑣 = 𝐵 → (2nd ‘𝑣) = (2nd ‘𝐵)) |
27 | 26 | eleq2d 2240 |
. . . . . . . 8
⊢ (𝑣 = 𝐵 → (𝑧 ∈ (2nd ‘𝑣) ↔ 𝑧 ∈ (2nd ‘𝐵))) |
28 | 27 | 3anbi2d 1312 |
. . . . . . 7
⊢ (𝑣 = 𝐵 → ((𝑦 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧)) ↔ (𝑦 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧)))) |
29 | 28 | 2rexbidv 2495 |
. . . . . 6
⊢ (𝑣 = 𝐵 → (∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd
‘𝐴) ∧ 𝑧 ∈ (2nd
‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧)) ↔ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd
‘𝐴) ∧ 𝑧 ∈ (2nd
‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧)))) |
30 | 29 | rabbidv 2719 |
. . . . 5
⊢ (𝑣 = 𝐵 → {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))} = {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ 𝑧 ∈
(2nd ‘𝐵)
∧ 𝑥 = (𝑦𝐺𝑧))}) |
31 | 25, 30 | opeq12d 3771 |
. . . 4
⊢ (𝑣 = 𝐵 → 〈{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(1st ‘𝐴)
∧ 𝑧 ∈
(1st ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉 = 〈{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(1st ‘𝐴)
∧ 𝑧 ∈
(1st ‘𝐵)
∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ 𝑧 ∈
(2nd ‘𝐵)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) |
32 | | genpelvl.1 |
. . . 4
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) |
33 | 20, 31, 32 | ovmpog 5985 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 〈{𝑥 ∈
Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st
‘𝐴) ∧ 𝑧 ∈ (1st
‘𝐵) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ 𝑧 ∈
(2nd ‘𝐵)
∧ 𝑥 = (𝑦𝐺𝑧))}〉 ∈ (𝒫 Q
× 𝒫 Q)) → (𝐴𝐹𝐵) = 〈{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(1st ‘𝐴)
∧ 𝑧 ∈
(1st ‘𝐵)
∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ 𝑧 ∈
(2nd ‘𝐵)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) |
34 | 9, 33 | mp3an3 1321 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴𝐹𝐵) = 〈{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(1st ‘𝐴)
∧ 𝑧 ∈
(1st ‘𝐵)
∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ 𝑧 ∈
(2nd ‘𝐵)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) |
35 | 34, 9 | eqeltrdi 2261 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴𝐹𝐵) ∈ (𝒫 Q ×
𝒫 Q)) |