Proof of Theorem genpelxp
Step | Hyp | Ref
| Expression |
1 | | ssrab2 3019 |
. . . . 5
⊢ {x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (1st ‘A) ∧ z ∈
(1st ‘B) ∧ x = (y𝐺z))}
⊆ Q |
2 | | nqex 6347 |
. . . . . 6
⊢
Q ∈ V |
3 | 2 | elpw2 3902 |
. . . . 5
⊢
({x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1st ‘A) ∧ z ∈ (1st ‘B) ∧ x = (y𝐺z))} ∈ 𝒫
Q ↔ {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1st ‘A) ∧ z ∈ (1st ‘B) ∧ x = (y𝐺z))} ⊆ Q) |
4 | 1, 3 | mpbir 134 |
. . . 4
⊢ {x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (1st ‘A) ∧ z ∈
(1st ‘B) ∧ x = (y𝐺z))}
∈ 𝒫 Q |
5 | | ssrab2 3019 |
. . . . 5
⊢ {x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (2nd ‘A) ∧ z ∈
(2nd ‘B) ∧ x = (y𝐺z))}
⊆ Q |
6 | 2 | elpw2 3902 |
. . . . 5
⊢
({x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2nd ‘A) ∧ z ∈ (2nd ‘B) ∧ x = (y𝐺z))} ∈ 𝒫
Q ↔ {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2nd ‘A) ∧ z ∈ (2nd ‘B) ∧ x = (y𝐺z))} ⊆ Q) |
7 | 5, 6 | mpbir 134 |
. . . 4
⊢ {x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (2nd ‘A) ∧ z ∈
(2nd ‘B) ∧ x = (y𝐺z))}
∈ 𝒫 Q |
8 | | opelxpi 4319 |
. . . 4
⊢
(({x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1st ‘A) ∧ z ∈ (1st ‘B) ∧ x = (y𝐺z))} ∈ 𝒫
Q ∧ {x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (2nd ‘A) ∧ z ∈
(2nd ‘B) ∧ x = (y𝐺z))}
∈ 𝒫 Q) →
〈{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1st ‘A) ∧ z ∈ (1st ‘B) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2nd ‘A) ∧ z ∈ (2nd ‘B) ∧ x = (y𝐺z))}〉 ∈
(𝒫 Q × 𝒫 Q)) |
9 | 4, 7, 8 | mp2an 402 |
. . 3
⊢
〈{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1st ‘A) ∧ z ∈ (1st ‘B) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2nd ‘A) ∧ z ∈ (2nd ‘B) ∧ x = (y𝐺z))}〉 ∈
(𝒫 Q × 𝒫 Q) |
10 | | fveq2 5121 |
. . . . . . . . 9
⊢ (w = A →
(1st ‘w) = (1st
‘A)) |
11 | 10 | eleq2d 2104 |
. . . . . . . 8
⊢ (w = A →
(y ∈
(1st ‘w) ↔ y ∈
(1st ‘A))) |
12 | 11 | 3anbi1d 1210 |
. . . . . . 7
⊢ (w = A →
((y ∈
(1st ‘w) ∧ z ∈ (1st ‘v) ∧ x = (y𝐺z)) ↔ (y
∈ (1st ‘A) ∧ z ∈
(1st ‘v) ∧ x = (y𝐺z)))) |
13 | 12 | 2rexbidv 2343 |
. . . . . 6
⊢ (w = A →
(∃y
∈ Q ∃z ∈ Q (y ∈
(1st ‘w) ∧ z ∈ (1st ‘v) ∧ x = (y𝐺z)) ↔ ∃y ∈ Q ∃z ∈ Q (y ∈
(1st ‘A) ∧ z ∈ (1st ‘v) ∧ x = (y𝐺z)))) |
14 | 13 | rabbidv 2543 |
. . . . 5
⊢ (w = A →
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (1st ‘w) ∧ z ∈
(1st ‘v) ∧ x = (y𝐺z))} =
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (1st ‘A) ∧ z ∈
(1st ‘v) ∧ x = (y𝐺z))}) |
15 | | fveq2 5121 |
. . . . . . . . 9
⊢ (w = A →
(2nd ‘w) = (2nd
‘A)) |
16 | 15 | eleq2d 2104 |
. . . . . . . 8
⊢ (w = A →
(y ∈
(2nd ‘w) ↔ y ∈
(2nd ‘A))) |
17 | 16 | 3anbi1d 1210 |
. . . . . . 7
⊢ (w = A →
((y ∈
(2nd ‘w) ∧ z ∈ (2nd ‘v) ∧ x = (y𝐺z)) ↔ (y
∈ (2nd ‘A) ∧ z ∈
(2nd ‘v) ∧ x = (y𝐺z)))) |
18 | 17 | 2rexbidv 2343 |
. . . . . 6
⊢ (w = A →
(∃y
∈ Q ∃z ∈ Q (y ∈
(2nd ‘w) ∧ z ∈ (2nd ‘v) ∧ x = (y𝐺z)) ↔ ∃y ∈ Q ∃z ∈ Q (y ∈
(2nd ‘A) ∧ z ∈ (2nd ‘v) ∧ x = (y𝐺z)))) |
19 | 18 | rabbidv 2543 |
. . . . 5
⊢ (w = A →
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (2nd ‘w) ∧ z ∈
(2nd ‘v) ∧ x = (y𝐺z))} =
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (2nd ‘A) ∧ z ∈
(2nd ‘v) ∧ x = (y𝐺z))}) |
20 | 14, 19 | opeq12d 3548 |
. . . 4
⊢ (w = A →
〈{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1st ‘w) ∧ z ∈ (1st ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2nd ‘w) ∧ z ∈ (2nd ‘v) ∧ x = (y𝐺z))}〉 = 〈{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (1st ‘A) ∧ z ∈
(1st ‘v) ∧ x = (y𝐺z))},
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (2nd ‘A) ∧ z ∈
(2nd ‘v) ∧ x = (y𝐺z))}〉) |
21 | | fveq2 5121 |
. . . . . . . . 9
⊢ (v = B →
(1st ‘v) = (1st
‘B)) |
22 | 21 | eleq2d 2104 |
. . . . . . . 8
⊢ (v = B →
(z ∈
(1st ‘v) ↔ z ∈
(1st ‘B))) |
23 | 22 | 3anbi2d 1211 |
. . . . . . 7
⊢ (v = B →
((y ∈
(1st ‘A) ∧ z ∈ (1st ‘v) ∧ x = (y𝐺z)) ↔ (y
∈ (1st ‘A) ∧ z ∈
(1st ‘B) ∧ x = (y𝐺z)))) |
24 | 23 | 2rexbidv 2343 |
. . . . . 6
⊢ (v = B →
(∃y
∈ Q ∃z ∈ Q (y ∈
(1st ‘A) ∧ z ∈ (1st ‘v) ∧ x = (y𝐺z)) ↔ ∃y ∈ Q ∃z ∈ Q (y ∈
(1st ‘A) ∧ z ∈ (1st ‘B) ∧ x = (y𝐺z)))) |
25 | 24 | rabbidv 2543 |
. . . . 5
⊢ (v = B →
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (1st ‘A) ∧ z ∈
(1st ‘v) ∧ x = (y𝐺z))} =
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (1st ‘A) ∧ z ∈
(1st ‘B) ∧ x = (y𝐺z))}) |
26 | | fveq2 5121 |
. . . . . . . . 9
⊢ (v = B →
(2nd ‘v) = (2nd
‘B)) |
27 | 26 | eleq2d 2104 |
. . . . . . . 8
⊢ (v = B →
(z ∈
(2nd ‘v) ↔ z ∈
(2nd ‘B))) |
28 | 27 | 3anbi2d 1211 |
. . . . . . 7
⊢ (v = B →
((y ∈
(2nd ‘A) ∧ z ∈ (2nd ‘v) ∧ x = (y𝐺z)) ↔ (y
∈ (2nd ‘A) ∧ z ∈
(2nd ‘B) ∧ x = (y𝐺z)))) |
29 | 28 | 2rexbidv 2343 |
. . . . . 6
⊢ (v = B →
(∃y
∈ Q ∃z ∈ Q (y ∈
(2nd ‘A) ∧ z ∈ (2nd ‘v) ∧ x = (y𝐺z)) ↔ ∃y ∈ Q ∃z ∈ Q (y ∈
(2nd ‘A) ∧ z ∈ (2nd ‘B) ∧ x = (y𝐺z)))) |
30 | 29 | rabbidv 2543 |
. . . . 5
⊢ (v = B →
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (2nd ‘A) ∧ z ∈
(2nd ‘v) ∧ x = (y𝐺z))} =
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (2nd ‘A) ∧ z ∈
(2nd ‘B) ∧ x = (y𝐺z))}) |
31 | 25, 30 | opeq12d 3548 |
. . . 4
⊢ (v = B →
〈{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1st ‘A) ∧ z ∈ (1st ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2nd ‘A) ∧ z ∈ (2nd ‘v) ∧ x = (y𝐺z))}〉 = 〈{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (1st ‘A) ∧ z ∈
(1st ‘B) ∧ x = (y𝐺z))},
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (2nd ‘A) ∧ z ∈
(2nd ‘B) ∧ x = (y𝐺z))}〉) |
32 | | genpelvl.1 |
. . . 4
⊢ 𝐹 = (w ∈
P, v ∈ P ↦ 〈{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (1st ‘w) ∧ z ∈
(1st ‘v) ∧ x = (y𝐺z))},
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (2nd ‘w) ∧ z ∈
(2nd ‘v) ∧ x = (y𝐺z))}〉) |
33 | 20, 31, 32 | ovmpt2g 5577 |
. . 3
⊢
((A ∈ P ∧ B ∈ P ∧ 〈{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1st ‘A) ∧ z ∈ (1st ‘B) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2nd ‘A) ∧ z ∈ (2nd ‘B) ∧ x = (y𝐺z))}〉 ∈
(𝒫 Q × 𝒫 Q)) → (A𝐹B) =
〈{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1st ‘A) ∧ z ∈ (1st ‘B) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2nd ‘A) ∧ z ∈ (2nd ‘B) ∧ x = (y𝐺z))}〉) |
34 | 9, 33 | mp3an3 1220 |
. 2
⊢
((A ∈ P ∧ B ∈ P) → (A𝐹B) =
〈{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1st ‘A) ∧ z ∈ (1st ‘B) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2nd ‘A) ∧ z ∈ (2nd ‘B) ∧ x = (y𝐺z))}〉) |
35 | 34, 9 | syl6eqel 2125 |
1
⊢
((A ∈ P ∧ B ∈ P) → (A𝐹B) ∈ (𝒫 Q × 𝒫
Q)) |