Step | Hyp | Ref
| Expression |
1 | | genpelvl.1 |
. . . . . . 7
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) |
2 | | genpelvl.2 |
. . . . . . 7
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) |
3 | 1, 2 | genipv 7431 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴𝐹𝐵) = 〈{𝑓 ∈ Q ∣ ∃𝑔 ∈ (1st
‘𝐴)∃ℎ ∈ (1st
‘𝐵)𝑓 = (𝑔𝐺ℎ)}, {𝑓 ∈ Q ∣ ∃𝑔 ∈ (2nd
‘𝐴)∃ℎ ∈ (2nd
‘𝐵)𝑓 = (𝑔𝐺ℎ)}〉) |
4 | 3 | fveq2d 5474 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (2nd ‘(𝐴𝐹𝐵)) = (2nd ‘〈{𝑓 ∈ Q ∣
∃𝑔 ∈
(1st ‘𝐴)∃ℎ ∈ (1st ‘𝐵)𝑓 = (𝑔𝐺ℎ)}, {𝑓 ∈ Q ∣ ∃𝑔 ∈ (2nd
‘𝐴)∃ℎ ∈ (2nd
‘𝐵)𝑓 = (𝑔𝐺ℎ)}〉)) |
5 | | nqex 7285 |
. . . . . . 7
⊢
Q ∈ V |
6 | 5 | rabex 4110 |
. . . . . 6
⊢ {𝑓 ∈ Q ∣
∃𝑔 ∈
(1st ‘𝐴)∃ℎ ∈ (1st ‘𝐵)𝑓 = (𝑔𝐺ℎ)} ∈ V |
7 | 5 | rabex 4110 |
. . . . . 6
⊢ {𝑓 ∈ Q ∣
∃𝑔 ∈
(2nd ‘𝐴)∃ℎ ∈ (2nd ‘𝐵)𝑓 = (𝑔𝐺ℎ)} ∈ V |
8 | 6, 7 | op2nd 6097 |
. . . . 5
⊢
(2nd ‘〈{𝑓 ∈ Q ∣ ∃𝑔 ∈ (1st
‘𝐴)∃ℎ ∈ (1st
‘𝐵)𝑓 = (𝑔𝐺ℎ)}, {𝑓 ∈ Q ∣ ∃𝑔 ∈ (2nd
‘𝐴)∃ℎ ∈ (2nd
‘𝐵)𝑓 = (𝑔𝐺ℎ)}〉) = {𝑓 ∈ Q ∣ ∃𝑔 ∈ (2nd
‘𝐴)∃ℎ ∈ (2nd
‘𝐵)𝑓 = (𝑔𝐺ℎ)} |
9 | 4, 8 | eqtrdi 2206 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (2nd ‘(𝐴𝐹𝐵)) = {𝑓 ∈ Q ∣ ∃𝑔 ∈ (2nd
‘𝐴)∃ℎ ∈ (2nd
‘𝐵)𝑓 = (𝑔𝐺ℎ)}) |
10 | 9 | eleq2d 2227 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐶 ∈
(2nd ‘(𝐴𝐹𝐵)) ↔ 𝐶 ∈ {𝑓 ∈ Q ∣ ∃𝑔 ∈ (2nd
‘𝐴)∃ℎ ∈ (2nd
‘𝐵)𝑓 = (𝑔𝐺ℎ)})) |
11 | | elrabi 2865 |
. . 3
⊢ (𝐶 ∈ {𝑓 ∈ Q ∣ ∃𝑔 ∈ (2nd
‘𝐴)∃ℎ ∈ (2nd
‘𝐵)𝑓 = (𝑔𝐺ℎ)} → 𝐶 ∈ Q) |
12 | 10, 11 | syl6bi 162 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐶 ∈
(2nd ‘(𝐴𝐹𝐵)) → 𝐶 ∈ Q)) |
13 | | prop 7397 |
. . . . . . 7
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
14 | | elprnqu 7404 |
. . . . . . 7
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑔 ∈ (2nd
‘𝐴)) → 𝑔 ∈
Q) |
15 | 13, 14 | sylan 281 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑔 ∈ (2nd
‘𝐴)) → 𝑔 ∈
Q) |
16 | | prop 7397 |
. . . . . . 7
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
17 | | elprnqu 7404 |
. . . . . . 7
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ ℎ ∈ (2nd
‘𝐵)) → ℎ ∈
Q) |
18 | 16, 17 | sylan 281 |
. . . . . 6
⊢ ((𝐵 ∈ P ∧
ℎ ∈ (2nd
‘𝐵)) → ℎ ∈
Q) |
19 | 2 | caovcl 5977 |
. . . . . 6
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔𝐺ℎ) ∈ Q) |
20 | 15, 18, 19 | syl2an 287 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ (2nd
‘𝐴)) ∧ (𝐵 ∈ P ∧
ℎ ∈ (2nd
‘𝐵))) → (𝑔𝐺ℎ) ∈ Q) |
21 | 20 | an4s 578 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑔 ∈
(2nd ‘𝐴)
∧ ℎ ∈
(2nd ‘𝐵)))
→ (𝑔𝐺ℎ) ∈ Q) |
22 | | eleq1 2220 |
. . . 4
⊢ (𝐶 = (𝑔𝐺ℎ) → (𝐶 ∈ Q ↔ (𝑔𝐺ℎ) ∈ Q)) |
23 | 21, 22 | syl5ibrcom 156 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑔 ∈
(2nd ‘𝐴)
∧ ℎ ∈
(2nd ‘𝐵)))
→ (𝐶 = (𝑔𝐺ℎ) → 𝐶 ∈ Q)) |
24 | 23 | rexlimdvva 2582 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (∃𝑔 ∈
(2nd ‘𝐴)∃ℎ ∈ (2nd ‘𝐵)𝐶 = (𝑔𝐺ℎ) → 𝐶 ∈ Q)) |
25 | | eqeq1 2164 |
. . . . . 6
⊢ (𝑓 = 𝐶 → (𝑓 = (𝑔𝐺ℎ) ↔ 𝐶 = (𝑔𝐺ℎ))) |
26 | 25 | 2rexbidv 2482 |
. . . . 5
⊢ (𝑓 = 𝐶 → (∃𝑔 ∈ (2nd ‘𝐴)∃ℎ ∈ (2nd ‘𝐵)𝑓 = (𝑔𝐺ℎ) ↔ ∃𝑔 ∈ (2nd ‘𝐴)∃ℎ ∈ (2nd ‘𝐵)𝐶 = (𝑔𝐺ℎ))) |
27 | 26 | elrab3 2869 |
. . . 4
⊢ (𝐶 ∈ Q →
(𝐶 ∈ {𝑓 ∈ Q ∣
∃𝑔 ∈
(2nd ‘𝐴)∃ℎ ∈ (2nd ‘𝐵)𝑓 = (𝑔𝐺ℎ)} ↔ ∃𝑔 ∈ (2nd ‘𝐴)∃ℎ ∈ (2nd ‘𝐵)𝐶 = (𝑔𝐺ℎ))) |
28 | 10, 27 | sylan9bb 458 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ 𝐶 ∈
Q) → (𝐶
∈ (2nd ‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (2nd ‘𝐴)∃ℎ ∈ (2nd ‘𝐵)𝐶 = (𝑔𝐺ℎ))) |
29 | 28 | ex 114 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐶 ∈
Q → (𝐶
∈ (2nd ‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (2nd ‘𝐴)∃ℎ ∈ (2nd ‘𝐵)𝐶 = (𝑔𝐺ℎ)))) |
30 | 12, 24, 29 | pm5.21ndd 695 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐶 ∈
(2nd ‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (2nd ‘𝐴)∃ℎ ∈ (2nd ‘𝐵)𝐶 = (𝑔𝐺ℎ))) |