Step | Hyp | Ref
| Expression |
1 | | oveq1 5519 |
. . . 4
⊢ (𝑓 = 𝐴 → (𝑓𝐹𝑔) = (𝐴𝐹𝑔)) |
2 | | fveq2 5178 |
. . . . . . 7
⊢ (𝑓 = 𝐴 → (1^{st} ‘𝑓) = (1^{st} ‘𝐴)) |
3 | 2 | rexeqdv 2512 |
. . . . . 6
⊢ (𝑓 = 𝐴 → (∃𝑦 ∈ (1^{st} ‘𝑓)∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ (1^{st} ‘𝐴)∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧))) |
4 | 3 | rabbidv 2549 |
. . . . 5
⊢ (𝑓 = 𝐴 → {𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝑓)∃𝑧 ∈ (1^{st}
‘𝑔)𝑥 = (𝑦𝐺𝑧)} = {𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝐴)∃𝑧 ∈ (1^{st}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}) |
5 | | fveq2 5178 |
. . . . . . 7
⊢ (𝑓 = 𝐴 → (2^{nd} ‘𝑓) = (2^{nd} ‘𝐴)) |
6 | 5 | rexeqdv 2512 |
. . . . . 6
⊢ (𝑓 = 𝐴 → (∃𝑦 ∈ (2^{nd} ‘𝑓)∃𝑧 ∈ (2^{nd} ‘𝑔)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ (2^{nd} ‘𝐴)∃𝑧 ∈ (2^{nd} ‘𝑔)𝑥 = (𝑦𝐺𝑧))) |
7 | 6 | rabbidv 2549 |
. . . . 5
⊢ (𝑓 = 𝐴 → {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)} = {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝐴)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}) |
8 | 4, 7 | opeq12d 3557 |
. . . 4
⊢ (𝑓 = 𝐴 → ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝑓)∃𝑧 ∈ (1^{st}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}⟩ = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝐴)∃𝑧 ∈ (1^{st}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝐴)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}⟩) |
9 | 1, 8 | eqeq12d 2054 |
. . 3
⊢ (𝑓 = 𝐴 → ((𝑓𝐹𝑔) = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝑓)∃𝑧 ∈ (1^{st}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}⟩ ↔ (𝐴𝐹𝑔) = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝐴)∃𝑧 ∈ (1^{st}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝐴)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}⟩)) |
10 | | oveq2 5520 |
. . . 4
⊢ (𝑔 = 𝐵 → (𝐴𝐹𝑔) = (𝐴𝐹𝐵)) |
11 | | fveq2 5178 |
. . . . . . . 8
⊢ (𝑔 = 𝐵 → (1^{st} ‘𝑔) = (1^{st} ‘𝐵)) |
12 | 11 | rexeqdv 2512 |
. . . . . . 7
⊢ (𝑔 = 𝐵 → (∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑧 ∈ (1^{st} ‘𝐵)𝑥 = (𝑦𝐺𝑧))) |
13 | 12 | rexbidv 2327 |
. . . . . 6
⊢ (𝑔 = 𝐵 → (∃𝑦 ∈ (1^{st} ‘𝐴)∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ (1^{st} ‘𝐴)∃𝑧 ∈ (1^{st} ‘𝐵)𝑥 = (𝑦𝐺𝑧))) |
14 | 13 | rabbidv 2549 |
. . . . 5
⊢ (𝑔 = 𝐵 → {𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝐴)∃𝑧 ∈ (1^{st}
‘𝑔)𝑥 = (𝑦𝐺𝑧)} = {𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝐴)∃𝑧 ∈ (1^{st}
‘𝐵)𝑥 = (𝑦𝐺𝑧)}) |
15 | | fveq2 5178 |
. . . . . . . 8
⊢ (𝑔 = 𝐵 → (2^{nd} ‘𝑔) = (2^{nd} ‘𝐵)) |
16 | 15 | rexeqdv 2512 |
. . . . . . 7
⊢ (𝑔 = 𝐵 → (∃𝑧 ∈ (2^{nd} ‘𝑔)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑧 ∈ (2^{nd} ‘𝐵)𝑥 = (𝑦𝐺𝑧))) |
17 | 16 | rexbidv 2327 |
. . . . . 6
⊢ (𝑔 = 𝐵 → (∃𝑦 ∈ (2^{nd} ‘𝐴)∃𝑧 ∈ (2^{nd} ‘𝑔)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ (2^{nd} ‘𝐴)∃𝑧 ∈ (2^{nd} ‘𝐵)𝑥 = (𝑦𝐺𝑧))) |
18 | 17 | rabbidv 2549 |
. . . . 5
⊢ (𝑔 = 𝐵 → {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝐴)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)} = {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝐴)∃𝑧 ∈ (2^{nd}
‘𝐵)𝑥 = (𝑦𝐺𝑧)}) |
19 | 14, 18 | opeq12d 3557 |
. . . 4
⊢ (𝑔 = 𝐵 → ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝐴)∃𝑧 ∈ (1^{st}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝐴)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}⟩ = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝐴)∃𝑧 ∈ (1^{st}
‘𝐵)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝐴)∃𝑧 ∈ (2^{nd}
‘𝐵)𝑥 = (𝑦𝐺𝑧)}⟩) |
20 | 10, 19 | eqeq12d 2054 |
. . 3
⊢ (𝑔 = 𝐵 → ((𝐴𝐹𝑔) = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝐴)∃𝑧 ∈ (1^{st}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝐴)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}⟩ ↔ (𝐴𝐹𝐵) = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝐴)∃𝑧 ∈ (1^{st}
‘𝐵)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝐴)∃𝑧 ∈ (2^{nd}
‘𝐵)𝑥 = (𝑦𝐺𝑧)}⟩)) |
21 | | nqex 6461 |
. . . . . . 7
⊢
Q ∈ V |
22 | 21 | a1i 9 |
. . . . . 6
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ Q ∈ V) |
23 | | rabssab 3027 |
. . . . . . 7
⊢ {𝑥 ∈ Q ∣
∃𝑦 ∈
(1^{st} ‘𝑓)∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧)} ⊆ {𝑥 ∣ ∃𝑦 ∈ (1^{st} ‘𝑓)∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧)} |
24 | | prop 6573 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ P →
⟨(1^{st} ‘𝑓), (2^{nd} ‘𝑓)⟩ ∈
P) |
25 | | elprnql 6579 |
. . . . . . . . . . . 12
⊢
((⟨(1^{st} ‘𝑓), (2^{nd} ‘𝑓)⟩ ∈ P ∧ 𝑦 ∈ (1^{st}
‘𝑓)) → 𝑦 ∈
Q) |
26 | 24, 25 | sylan 267 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ P ∧
𝑦 ∈ (1^{st}
‘𝑓)) → 𝑦 ∈
Q) |
27 | | prop 6573 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ P →
⟨(1^{st} ‘𝑔), (2^{nd} ‘𝑔)⟩ ∈
P) |
28 | | elprnql 6579 |
. . . . . . . . . . . 12
⊢
((⟨(1^{st} ‘𝑔), (2^{nd} ‘𝑔)⟩ ∈ P ∧ 𝑧 ∈ (1^{st}
‘𝑔)) → 𝑧 ∈
Q) |
29 | 27, 28 | sylan 267 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ P ∧
𝑧 ∈ (1^{st}
‘𝑔)) → 𝑧 ∈
Q) |
30 | | genp.2 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) |
31 | | eleq1 2100 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦𝐺𝑧) → (𝑥 ∈ Q ↔ (𝑦𝐺𝑧) ∈ Q)) |
32 | 30, 31 | syl5ibrcom 146 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑥 = (𝑦𝐺𝑧) → 𝑥 ∈ Q)) |
33 | 26, 29, 32 | syl2an 273 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ P ∧
𝑦 ∈ (1^{st}
‘𝑓)) ∧ (𝑔 ∈ P ∧
𝑧 ∈ (1^{st}
‘𝑔))) → (𝑥 = (𝑦𝐺𝑧) → 𝑥 ∈ Q)) |
34 | 33 | an4s 522 |
. . . . . . . . 9
⊢ (((𝑓 ∈ P ∧
𝑔 ∈ P)
∧ (𝑦 ∈
(1^{st} ‘𝑓)
∧ 𝑧 ∈
(1^{st} ‘𝑔)))
→ (𝑥 = (𝑦𝐺𝑧) → 𝑥 ∈ Q)) |
35 | 34 | rexlimdvva 2440 |
. . . . . . . 8
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (∃𝑦 ∈
(1^{st} ‘𝑓)∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧) → 𝑥 ∈ Q)) |
36 | 35 | abssdv 3014 |
. . . . . . 7
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ {𝑥 ∣
∃𝑦 ∈
(1^{st} ‘𝑓)∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧)} ⊆ Q) |
37 | 23, 36 | syl5ss 2956 |
. . . . . 6
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ {𝑥 ∈
Q ∣ ∃𝑦 ∈ (1^{st} ‘𝑓)∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧)} ⊆ Q) |
38 | 22, 37 | ssexd 3897 |
. . . . 5
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ {𝑥 ∈
Q ∣ ∃𝑦 ∈ (1^{st} ‘𝑓)∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧)} ∈ V) |
39 | | rabssab 3027 |
. . . . . . 7
⊢ {𝑥 ∈ Q ∣
∃𝑦 ∈
(2^{nd} ‘𝑓)∃𝑧 ∈ (2^{nd} ‘𝑔)𝑥 = (𝑦𝐺𝑧)} ⊆ {𝑥 ∣ ∃𝑦 ∈ (2^{nd} ‘𝑓)∃𝑧 ∈ (2^{nd} ‘𝑔)𝑥 = (𝑦𝐺𝑧)} |
40 | | elprnqu 6580 |
. . . . . . . . . . . 12
⊢
((⟨(1^{st} ‘𝑓), (2^{nd} ‘𝑓)⟩ ∈ P ∧ 𝑦 ∈ (2^{nd}
‘𝑓)) → 𝑦 ∈
Q) |
41 | 24, 40 | sylan 267 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ P ∧
𝑦 ∈ (2^{nd}
‘𝑓)) → 𝑦 ∈
Q) |
42 | | elprnqu 6580 |
. . . . . . . . . . . 12
⊢
((⟨(1^{st} ‘𝑔), (2^{nd} ‘𝑔)⟩ ∈ P ∧ 𝑧 ∈ (2^{nd}
‘𝑔)) → 𝑧 ∈
Q) |
43 | 27, 42 | sylan 267 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ P ∧
𝑧 ∈ (2^{nd}
‘𝑔)) → 𝑧 ∈
Q) |
44 | 41, 43, 32 | syl2an 273 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ P ∧
𝑦 ∈ (2^{nd}
‘𝑓)) ∧ (𝑔 ∈ P ∧
𝑧 ∈ (2^{nd}
‘𝑔))) → (𝑥 = (𝑦𝐺𝑧) → 𝑥 ∈ Q)) |
45 | 44 | an4s 522 |
. . . . . . . . 9
⊢ (((𝑓 ∈ P ∧
𝑔 ∈ P)
∧ (𝑦 ∈
(2^{nd} ‘𝑓)
∧ 𝑧 ∈
(2^{nd} ‘𝑔)))
→ (𝑥 = (𝑦𝐺𝑧) → 𝑥 ∈ Q)) |
46 | 45 | rexlimdvva 2440 |
. . . . . . . 8
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (∃𝑦 ∈
(2^{nd} ‘𝑓)∃𝑧 ∈ (2^{nd} ‘𝑔)𝑥 = (𝑦𝐺𝑧) → 𝑥 ∈ Q)) |
47 | 46 | abssdv 3014 |
. . . . . . 7
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ {𝑥 ∣
∃𝑦 ∈
(2^{nd} ‘𝑓)∃𝑧 ∈ (2^{nd} ‘𝑔)𝑥 = (𝑦𝐺𝑧)} ⊆ Q) |
48 | 39, 47 | syl5ss 2956 |
. . . . . 6
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ {𝑥 ∈
Q ∣ ∃𝑦 ∈ (2^{nd} ‘𝑓)∃𝑧 ∈ (2^{nd} ‘𝑔)𝑥 = (𝑦𝐺𝑧)} ⊆ Q) |
49 | 22, 48 | ssexd 3897 |
. . . . 5
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ {𝑥 ∈
Q ∣ ∃𝑦 ∈ (2^{nd} ‘𝑓)∃𝑧 ∈ (2^{nd} ‘𝑔)𝑥 = (𝑦𝐺𝑧)} ∈ V) |
50 | | opelxp 4374 |
. . . . 5
⊢
(⟨{𝑥 ∈
Q ∣ ∃𝑦 ∈ (1^{st} ‘𝑓)∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}⟩ ∈ (V × V) ↔ ({𝑥 ∈ Q ∣
∃𝑦 ∈
(1^{st} ‘𝑓)∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧)} ∈ V ∧ {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)} ∈ V)) |
51 | 38, 49, 50 | sylanbrc 394 |
. . . 4
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ ⟨{𝑥 ∈
Q ∣ ∃𝑦 ∈ (1^{st} ‘𝑓)∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}⟩ ∈ (V ×
V)) |
52 | | fveq2 5178 |
. . . . . . . 8
⊢ (𝑤 = 𝑓 → (1^{st} ‘𝑤) = (1^{st} ‘𝑓)) |
53 | 52 | rexeqdv 2512 |
. . . . . . 7
⊢ (𝑤 = 𝑓 → (∃𝑦 ∈ (1^{st} ‘𝑤)∃𝑧 ∈ (1^{st} ‘𝑣)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ (1^{st} ‘𝑓)∃𝑧 ∈ (1^{st} ‘𝑣)𝑥 = (𝑦𝐺𝑧))) |
54 | 53 | rabbidv 2549 |
. . . . . 6
⊢ (𝑤 = 𝑓 → {𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝑤)∃𝑧 ∈ (1^{st}
‘𝑣)𝑥 = (𝑦𝐺𝑧)} = {𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝑓)∃𝑧 ∈ (1^{st}
‘𝑣)𝑥 = (𝑦𝐺𝑧)}) |
55 | | fveq2 5178 |
. . . . . . . 8
⊢ (𝑤 = 𝑓 → (2^{nd} ‘𝑤) = (2^{nd} ‘𝑓)) |
56 | 55 | rexeqdv 2512 |
. . . . . . 7
⊢ (𝑤 = 𝑓 → (∃𝑦 ∈ (2^{nd} ‘𝑤)∃𝑧 ∈ (2^{nd} ‘𝑣)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ (2^{nd} ‘𝑓)∃𝑧 ∈ (2^{nd} ‘𝑣)𝑥 = (𝑦𝐺𝑧))) |
57 | 56 | rabbidv 2549 |
. . . . . 6
⊢ (𝑤 = 𝑓 → {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑤)∃𝑧 ∈ (2^{nd}
‘𝑣)𝑥 = (𝑦𝐺𝑧)} = {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑣)𝑥 = (𝑦𝐺𝑧)}) |
58 | 54, 57 | opeq12d 3557 |
. . . . 5
⊢ (𝑤 = 𝑓 → ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝑤)∃𝑧 ∈ (1^{st}
‘𝑣)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑤)∃𝑧 ∈ (2^{nd}
‘𝑣)𝑥 = (𝑦𝐺𝑧)}⟩ = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝑓)∃𝑧 ∈ (1^{st}
‘𝑣)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑣)𝑥 = (𝑦𝐺𝑧)}⟩) |
59 | | fveq2 5178 |
. . . . . . . . 9
⊢ (𝑣 = 𝑔 → (1^{st} ‘𝑣) = (1^{st} ‘𝑔)) |
60 | 59 | rexeqdv 2512 |
. . . . . . . 8
⊢ (𝑣 = 𝑔 → (∃𝑧 ∈ (1^{st} ‘𝑣)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧))) |
61 | 60 | rexbidv 2327 |
. . . . . . 7
⊢ (𝑣 = 𝑔 → (∃𝑦 ∈ (1^{st} ‘𝑓)∃𝑧 ∈ (1^{st} ‘𝑣)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ (1^{st} ‘𝑓)∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧))) |
62 | 61 | rabbidv 2549 |
. . . . . 6
⊢ (𝑣 = 𝑔 → {𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝑓)∃𝑧 ∈ (1^{st}
‘𝑣)𝑥 = (𝑦𝐺𝑧)} = {𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝑓)∃𝑧 ∈ (1^{st}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}) |
63 | | fveq2 5178 |
. . . . . . . . 9
⊢ (𝑣 = 𝑔 → (2^{nd} ‘𝑣) = (2^{nd} ‘𝑔)) |
64 | 63 | rexeqdv 2512 |
. . . . . . . 8
⊢ (𝑣 = 𝑔 → (∃𝑧 ∈ (2^{nd} ‘𝑣)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑧 ∈ (2^{nd} ‘𝑔)𝑥 = (𝑦𝐺𝑧))) |
65 | 64 | rexbidv 2327 |
. . . . . . 7
⊢ (𝑣 = 𝑔 → (∃𝑦 ∈ (2^{nd} ‘𝑓)∃𝑧 ∈ (2^{nd} ‘𝑣)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ (2^{nd} ‘𝑓)∃𝑧 ∈ (2^{nd} ‘𝑔)𝑥 = (𝑦𝐺𝑧))) |
66 | 65 | rabbidv 2549 |
. . . . . 6
⊢ (𝑣 = 𝑔 → {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑣)𝑥 = (𝑦𝐺𝑧)} = {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}) |
67 | 62, 66 | opeq12d 3557 |
. . . . 5
⊢ (𝑣 = 𝑔 → ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝑓)∃𝑧 ∈ (1^{st}
‘𝑣)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑣)𝑥 = (𝑦𝐺𝑧)}⟩ = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝑓)∃𝑧 ∈ (1^{st}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}⟩) |
68 | | genp.1 |
. . . . . 6
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) |
69 | 68 | genpdf 6606 |
. . . . 5
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
(1^{st} ‘𝑤)∃𝑧 ∈ (1^{st} ‘𝑣)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑤)∃𝑧 ∈ (2^{nd}
‘𝑣)𝑥 = (𝑦𝐺𝑧)}⟩) |
70 | 58, 67, 69 | ovmpt2g 5635 |
. . . 4
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P
∧ ⟨{𝑥 ∈
Q ∣ ∃𝑦 ∈ (1^{st} ‘𝑓)∃𝑧 ∈ (1^{st} ‘𝑔)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}⟩ ∈ (V × V)) → (𝑓𝐹𝑔) = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝑓)∃𝑧 ∈ (1^{st}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}⟩) |
71 | 51, 70 | mpd3an3 1233 |
. . 3
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (𝑓𝐹𝑔) = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝑓)∃𝑧 ∈ (1^{st}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝑓)∃𝑧 ∈ (2^{nd}
‘𝑔)𝑥 = (𝑦𝐺𝑧)}⟩) |
72 | 9, 20, 71 | vtocl2ga 2621 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴𝐹𝐵) = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝐴)∃𝑧 ∈ (1^{st}
‘𝐵)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝐴)∃𝑧 ∈ (2^{nd}
‘𝐵)𝑥 = (𝑦𝐺𝑧)}⟩) |
73 | | eqeq1 2046 |
. . . . . 6
⊢ (𝑥 = 𝑞 → (𝑥 = (𝑦𝐺𝑧) ↔ 𝑞 = (𝑦𝐺𝑧))) |
74 | 73 | 2rexbidv 2349 |
. . . . 5
⊢ (𝑥 = 𝑞 → (∃𝑦 ∈ (1^{st} ‘𝐴)∃𝑧 ∈ (1^{st} ‘𝐵)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ (1^{st} ‘𝐴)∃𝑧 ∈ (1^{st} ‘𝐵)𝑞 = (𝑦𝐺𝑧))) |
75 | | oveq1 5519 |
. . . . . . 7
⊢ (𝑦 = 𝑟 → (𝑦𝐺𝑧) = (𝑟𝐺𝑧)) |
76 | 75 | eqeq2d 2051 |
. . . . . 6
⊢ (𝑦 = 𝑟 → (𝑞 = (𝑦𝐺𝑧) ↔ 𝑞 = (𝑟𝐺𝑧))) |
77 | | oveq2 5520 |
. . . . . . 7
⊢ (𝑧 = 𝑠 → (𝑟𝐺𝑧) = (𝑟𝐺𝑠)) |
78 | 77 | eqeq2d 2051 |
. . . . . 6
⊢ (𝑧 = 𝑠 → (𝑞 = (𝑟𝐺𝑧) ↔ 𝑞 = (𝑟𝐺𝑠))) |
79 | 76, 78 | cbvrex2v 2542 |
. . . . 5
⊢
(∃𝑦 ∈
(1^{st} ‘𝐴)∃𝑧 ∈ (1^{st} ‘𝐵)𝑞 = (𝑦𝐺𝑧) ↔ ∃𝑟 ∈ (1^{st} ‘𝐴)∃𝑠 ∈ (1^{st} ‘𝐵)𝑞 = (𝑟𝐺𝑠)) |
80 | 74, 79 | syl6bb 185 |
. . . 4
⊢ (𝑥 = 𝑞 → (∃𝑦 ∈ (1^{st} ‘𝐴)∃𝑧 ∈ (1^{st} ‘𝐵)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑟 ∈ (1^{st} ‘𝐴)∃𝑠 ∈ (1^{st} ‘𝐵)𝑞 = (𝑟𝐺𝑠))) |
81 | 80 | cbvrabv 2556 |
. . 3
⊢ {𝑥 ∈ Q ∣
∃𝑦 ∈
(1^{st} ‘𝐴)∃𝑧 ∈ (1^{st} ‘𝐵)𝑥 = (𝑦𝐺𝑧)} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ (1^{st}
‘𝐴)∃𝑠 ∈ (1^{st}
‘𝐵)𝑞 = (𝑟𝐺𝑠)} |
82 | 73 | 2rexbidv 2349 |
. . . . 5
⊢ (𝑥 = 𝑞 → (∃𝑦 ∈ (2^{nd} ‘𝐴)∃𝑧 ∈ (2^{nd} ‘𝐵)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ (2^{nd} ‘𝐴)∃𝑧 ∈ (2^{nd} ‘𝐵)𝑞 = (𝑦𝐺𝑧))) |
83 | 76, 78 | cbvrex2v 2542 |
. . . . 5
⊢
(∃𝑦 ∈
(2^{nd} ‘𝐴)∃𝑧 ∈ (2^{nd} ‘𝐵)𝑞 = (𝑦𝐺𝑧) ↔ ∃𝑟 ∈ (2^{nd} ‘𝐴)∃𝑠 ∈ (2^{nd} ‘𝐵)𝑞 = (𝑟𝐺𝑠)) |
84 | 82, 83 | syl6bb 185 |
. . . 4
⊢ (𝑥 = 𝑞 → (∃𝑦 ∈ (2^{nd} ‘𝐴)∃𝑧 ∈ (2^{nd} ‘𝐵)𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑟 ∈ (2^{nd} ‘𝐴)∃𝑠 ∈ (2^{nd} ‘𝐵)𝑞 = (𝑟𝐺𝑠))) |
85 | 84 | cbvrabv 2556 |
. . 3
⊢ {𝑥 ∈ Q ∣
∃𝑦 ∈
(2^{nd} ‘𝐴)∃𝑧 ∈ (2^{nd} ‘𝐵)𝑥 = (𝑦𝐺𝑧)} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ (2^{nd}
‘𝐴)∃𝑠 ∈ (2^{nd}
‘𝐵)𝑞 = (𝑟𝐺𝑠)} |
86 | 81, 85 | opeq12i 3554 |
. 2
⊢
⟨{𝑥 ∈
Q ∣ ∃𝑦 ∈ (1^{st} ‘𝐴)∃𝑧 ∈ (1^{st} ‘𝐵)𝑥 = (𝑦𝐺𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝐴)∃𝑧 ∈ (2^{nd}
‘𝐵)𝑥 = (𝑦𝐺𝑧)}⟩ = ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ (1^{st}
‘𝐴)∃𝑠 ∈ (1^{st}
‘𝐵)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ (2^{nd}
‘𝐴)∃𝑠 ∈ (2^{nd}
‘𝐵)𝑞 = (𝑟𝐺𝑠)}⟩ |
87 | 72, 86 | syl6eq 2088 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴𝐹𝐵) = ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ (1^{st}
‘𝐴)∃𝑠 ∈ (1^{st}
‘𝐵)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ (2^{nd}
‘𝐴)∃𝑠 ∈ (2^{nd}
‘𝐵)𝑞 = (𝑟𝐺𝑠)}⟩) |