Step | Hyp | Ref
| Expression |
1 | | genpelvl.1 |
. . . . . . 7
⊢ 𝐹 = (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))}〉) |
2 | | genpelvl.2 |
. . . . . . 7
⊢
((y ∈ Q ∧ z ∈ Q) → (y𝐺z) ∈ Q) |
3 | 1, 2 | genipv 6492 |
. . . . . 6
⊢
((A ∈ P ∧ B ∈ P) → (A𝐹B) =
〈{f ∈ Q ∣ ∃g ∈ (1st ‘A)∃ℎ ∈
(1st ‘B)f = (g𝐺ℎ)}, {f
∈ Q ∣ ∃g ∈ (2nd ‘A)∃ℎ ∈
(2nd ‘B)f = (g𝐺ℎ)}〉) |
4 | 3 | fveq2d 5125 |
. . . . 5
⊢
((A ∈ P ∧ B ∈ P) → (1st
‘(A𝐹B)) =
(1st ‘〈{f ∈ Q ∣ ∃g ∈ (1st ‘A)∃ℎ ∈
(1st ‘B)f = (g𝐺ℎ)}, {f
∈ Q ∣ ∃g ∈ (2nd ‘A)∃ℎ ∈
(2nd ‘B)f = (g𝐺ℎ)}〉)) |
5 | | nqex 6347 |
. . . . . . 7
⊢
Q ∈ V |
6 | 5 | rabex 3892 |
. . . . . 6
⊢ {f ∈
Q ∣ ∃g ∈
(1st ‘A)∃ℎ
∈ (1st ‘B)f = (g𝐺ℎ)} ∈
V |
7 | 5 | rabex 3892 |
. . . . . 6
⊢ {f ∈
Q ∣ ∃g ∈
(2nd ‘A)∃ℎ
∈ (2nd ‘B)f = (g𝐺ℎ)} ∈
V |
8 | 6, 7 | op1st 5715 |
. . . . 5
⊢
(1st ‘〈{f
∈ Q ∣ ∃g ∈ (1st ‘A)∃ℎ ∈
(1st ‘B)f = (g𝐺ℎ)}, {f
∈ Q ∣ ∃g ∈ (2nd ‘A)∃ℎ ∈
(2nd ‘B)f = (g𝐺ℎ)}〉) = {f ∈
Q ∣ ∃g ∈
(1st ‘A)∃ℎ
∈ (1st ‘B)f = (g𝐺ℎ)} |
9 | 4, 8 | syl6eq 2085 |
. . . 4
⊢
((A ∈ P ∧ B ∈ P) → (1st
‘(A𝐹B)) =
{f ∈
Q ∣ ∃g ∈
(1st ‘A)∃ℎ
∈ (1st ‘B)f = (g𝐺ℎ)}) |
10 | 9 | eleq2d 2104 |
. . 3
⊢
((A ∈ P ∧ B ∈ P) → (𝐶 ∈
(1st ‘(A𝐹B))
↔ 𝐶 ∈ {f ∈ Q ∣ ∃g ∈ (1st ‘A)∃ℎ ∈
(1st ‘B)f = (g𝐺ℎ)})) |
11 | | elrabi 2689 |
. . 3
⊢ (𝐶 ∈ {f ∈ Q ∣ ∃g ∈ (1st ‘A)∃ℎ ∈
(1st ‘B)f = (g𝐺ℎ)} → 𝐶 ∈
Q) |
12 | 10, 11 | syl6bi 152 |
. 2
⊢
((A ∈ P ∧ B ∈ P) → (𝐶 ∈
(1st ‘(A𝐹B))
→ 𝐶 ∈ Q)) |
13 | | prop 6458 |
. . . . . . 7
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
14 | | elprnql 6464 |
. . . . . . 7
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ g ∈ (1st ‘A)) → g
∈ Q) |
15 | 13, 14 | sylan 267 |
. . . . . 6
⊢
((A ∈ P ∧ g ∈ (1st ‘A)) → g
∈ Q) |
16 | | prop 6458 |
. . . . . . 7
⊢ (B ∈
P → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
17 | | elprnql 6464 |
. . . . . . 7
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ ℎ
∈ (1st ‘B)) → ℎ ∈
Q) |
18 | 16, 17 | sylan 267 |
. . . . . 6
⊢
((B ∈ P ∧ ℎ
∈ (1st ‘B)) → ℎ ∈
Q) |
19 | 2 | caovcl 5597 |
. . . . . 6
⊢
((g ∈ Q ∧ ℎ
∈ Q) → (g𝐺ℎ) ∈
Q) |
20 | 15, 18, 19 | syl2an 273 |
. . . . 5
⊢
(((A ∈ P ∧ g ∈ (1st ‘A)) ∧ (B ∈
P ∧ ℎ ∈
(1st ‘B))) →
(g𝐺ℎ) ∈
Q) |
21 | 20 | an4s 522 |
. . . 4
⊢
(((A ∈ P ∧ B ∈ P) ∧ (g ∈ (1st ‘A) ∧ ℎ ∈
(1st ‘B))) →
(g𝐺ℎ) ∈
Q) |
22 | | eleq1 2097 |
. . . 4
⊢ (𝐶 = (g𝐺ℎ) → (𝐶 ∈
Q ↔ (g𝐺ℎ) ∈
Q)) |
23 | 21, 22 | syl5ibrcom 146 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P) ∧ (g ∈ (1st ‘A) ∧ ℎ ∈
(1st ‘B))) → (𝐶 = (g𝐺ℎ) → 𝐶 ∈
Q)) |
24 | 23 | rexlimdvva 2434 |
. 2
⊢
((A ∈ P ∧ B ∈ P) → (∃g ∈ (1st ‘A)∃ℎ ∈
(1st ‘B)𝐶 = (g𝐺ℎ) → 𝐶 ∈
Q)) |
25 | | eqeq1 2043 |
. . . . . 6
⊢ (f = 𝐶 → (f = (g𝐺ℎ) ↔ 𝐶 = (g𝐺ℎ))) |
26 | 25 | 2rexbidv 2343 |
. . . . 5
⊢ (f = 𝐶 → (∃g ∈ (1st ‘A)∃ℎ ∈
(1st ‘B)f = (g𝐺ℎ) ↔ ∃g ∈ (1st ‘A)∃ℎ ∈
(1st ‘B)𝐶 = (g𝐺ℎ))) |
27 | 26 | elrab3 2693 |
. . . 4
⊢ (𝐶 ∈ Q → (𝐶 ∈
{f ∈
Q ∣ ∃g ∈
(1st ‘A)∃ℎ
∈ (1st ‘B)f = (g𝐺ℎ)} ↔ ∃g ∈ (1st ‘A)∃ℎ ∈
(1st ‘B)𝐶 = (g𝐺ℎ))) |
28 | 10, 27 | sylan9bb 435 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P) ∧ 𝐶 ∈
Q) → (𝐶
∈ (1st ‘(A𝐹B))
↔ ∃g ∈
(1st ‘A)∃ℎ
∈ (1st ‘B)𝐶 = (g𝐺ℎ))) |
29 | 28 | ex 108 |
. 2
⊢
((A ∈ P ∧ B ∈ P) → (𝐶 ∈
Q → (𝐶
∈ (1st ‘(A𝐹B))
↔ ∃g ∈
(1st ‘A)∃ℎ
∈ (1st ‘B)𝐶 = (g𝐺ℎ)))) |
30 | 12, 24, 29 | pm5.21ndd 620 |
1
⊢
((A ∈ P ∧ B ∈ P) → (𝐶 ∈
(1st ‘(A𝐹B))
↔ ∃g ∈
(1st ‘A)∃ℎ
∈ (1st ‘B)𝐶 = (g𝐺ℎ))) |