Step | Hyp | Ref
| Expression |
1 | | oveq1 5462 |
. . . 4
⊢ (f = A →
(f𝐹g) =
(A𝐹g)) |
2 | | fveq2 5121 |
. . . . . . 7
⊢ (f = A →
(1^{st} ‘f) = (1^{st}
‘A)) |
3 | 2 | rexeqdv 2506 |
. . . . . 6
⊢ (f = A →
(∃y
∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘g)x = (y𝐺z) ↔ ∃y ∈ (1^{st} ‘A)∃z ∈
(1^{st} ‘g)x = (y𝐺z))) |
4 | 3 | rabbidv 2543 |
. . . . 5
⊢ (f = A →
{x ∈
Q ∣ ∃y ∈
(1^{st} ‘f)∃z ∈ (1^{st} ‘g)x = (y𝐺z)} =
{x ∈
Q ∣ ∃y ∈
(1^{st} ‘A)∃z ∈ (1^{st} ‘g)x = (y𝐺z)}) |
5 | | fveq2 5121 |
. . . . . . 7
⊢ (f = A →
(2^{nd} ‘f) = (2^{nd}
‘A)) |
6 | 5 | rexeqdv 2506 |
. . . . . 6
⊢ (f = A →
(∃y
∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘g)x = (y𝐺z) ↔ ∃y ∈ (2^{nd} ‘A)∃z ∈
(2^{nd} ‘g)x = (y𝐺z))) |
7 | 6 | rabbidv 2543 |
. . . . 5
⊢ (f = A →
{x ∈
Q ∣ ∃y ∈
(2^{nd} ‘f)∃z ∈ (2^{nd} ‘g)x = (y𝐺z)} =
{x ∈
Q ∣ ∃y ∈
(2^{nd} ‘A)∃z ∈ (2^{nd} ‘g)x = (y𝐺z)}) |
8 | 4, 7 | opeq12d 3548 |
. . . 4
⊢ (f = A →
⟨{x ∈ Q ∣ ∃y ∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘g)x = (y𝐺z)}⟩ = ⟨{x ∈
Q ∣ ∃y ∈
(1^{st} ‘A)∃z ∈ (1^{st} ‘g)x = (y𝐺z)},
{x ∈
Q ∣ ∃y ∈
(2^{nd} ‘A)∃z ∈ (2^{nd} ‘g)x = (y𝐺z)}⟩) |
9 | 1, 8 | eqeq12d 2051 |
. . 3
⊢ (f = A →
((f𝐹g) =
⟨{x ∈ Q ∣ ∃y ∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘g)x = (y𝐺z)}⟩ ↔ (A𝐹g) =
⟨{x ∈ Q ∣ ∃y ∈ (1^{st} ‘A)∃z ∈
(1^{st} ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘A)∃z ∈
(2^{nd} ‘g)x = (y𝐺z)}⟩)) |
10 | | oveq2 5463 |
. . . 4
⊢ (g = B →
(A𝐹g) =
(A𝐹B)) |
11 | | fveq2 5121 |
. . . . . . . 8
⊢ (g = B →
(1^{st} ‘g) = (1^{st}
‘B)) |
12 | 11 | rexeqdv 2506 |
. . . . . . 7
⊢ (g = B →
(∃z
∈ (1^{st} ‘g)x = (y𝐺z)
↔ ∃z ∈
(1^{st} ‘B)x = (y𝐺z))) |
13 | 12 | rexbidv 2321 |
. . . . . 6
⊢ (g = B →
(∃y
∈ (1^{st} ‘A)∃z ∈
(1^{st} ‘g)x = (y𝐺z) ↔ ∃y ∈ (1^{st} ‘A)∃z ∈
(1^{st} ‘B)x = (y𝐺z))) |
14 | 13 | rabbidv 2543 |
. . . . 5
⊢ (g = B →
{x ∈
Q ∣ ∃y ∈
(1^{st} ‘A)∃z ∈ (1^{st} ‘g)x = (y𝐺z)} =
{x ∈
Q ∣ ∃y ∈
(1^{st} ‘A)∃z ∈ (1^{st} ‘B)x = (y𝐺z)}) |
15 | | fveq2 5121 |
. . . . . . . 8
⊢ (g = B →
(2^{nd} ‘g) = (2^{nd}
‘B)) |
16 | 15 | rexeqdv 2506 |
. . . . . . 7
⊢ (g = B →
(∃z
∈ (2^{nd} ‘g)x = (y𝐺z)
↔ ∃z ∈
(2^{nd} ‘B)x = (y𝐺z))) |
17 | 16 | rexbidv 2321 |
. . . . . 6
⊢ (g = B →
(∃y
∈ (2^{nd} ‘A)∃z ∈
(2^{nd} ‘g)x = (y𝐺z) ↔ ∃y ∈ (2^{nd} ‘A)∃z ∈
(2^{nd} ‘B)x = (y𝐺z))) |
18 | 17 | rabbidv 2543 |
. . . . 5
⊢ (g = B →
{x ∈
Q ∣ ∃y ∈
(2^{nd} ‘A)∃z ∈ (2^{nd} ‘g)x = (y𝐺z)} =
{x ∈
Q ∣ ∃y ∈
(2^{nd} ‘A)∃z ∈ (2^{nd} ‘B)x = (y𝐺z)}) |
19 | 14, 18 | opeq12d 3548 |
. . . 4
⊢ (g = B →
⟨{x ∈ Q ∣ ∃y ∈ (1^{st} ‘A)∃z ∈
(1^{st} ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘A)∃z ∈
(2^{nd} ‘g)x = (y𝐺z)}⟩ = ⟨{x ∈
Q ∣ ∃y ∈
(1^{st} ‘A)∃z ∈ (1^{st} ‘B)x = (y𝐺z)},
{x ∈
Q ∣ ∃y ∈
(2^{nd} ‘A)∃z ∈ (2^{nd} ‘B)x = (y𝐺z)}⟩) |
20 | 10, 19 | eqeq12d 2051 |
. . 3
⊢ (g = B →
((A𝐹g) =
⟨{x ∈ Q ∣ ∃y ∈ (1^{st} ‘A)∃z ∈
(1^{st} ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘A)∃z ∈
(2^{nd} ‘g)x = (y𝐺z)}⟩ ↔ (A𝐹B) =
⟨{x ∈ Q ∣ ∃y ∈ (1^{st} ‘A)∃z ∈
(1^{st} ‘B)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘A)∃z ∈
(2^{nd} ‘B)x = (y𝐺z)}⟩)) |
21 | | nqex 6347 |
. . . . . . 7
⊢
Q ∈ V |
22 | 21 | a1i 9 |
. . . . . 6
⊢
((f ∈ P ∧ g ∈ P) → Q ∈ V) |
23 | | rabssab 3021 |
. . . . . . 7
⊢ {x ∈
Q ∣ ∃y ∈
(1^{st} ‘f)∃z ∈ (1^{st} ‘g)x = (y𝐺z)}
⊆ {x ∣ ∃y ∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘g)x = (y𝐺z)} |
24 | | prop 6457 |
. . . . . . . . . . . 12
⊢ (f ∈
P → ⟨(1^{st} ‘f), (2^{nd} ‘f)⟩ ∈
P) |
25 | | elprnql 6463 |
. . . . . . . . . . . 12
⊢
((⟨(1^{st} ‘f),
(2^{nd} ‘f)⟩ ∈ P ∧ y ∈ (1^{st} ‘f)) → y
∈ Q) |
26 | 24, 25 | sylan 267 |
. . . . . . . . . . 11
⊢
((f ∈ P ∧ y ∈ (1^{st} ‘f)) → y
∈ Q) |
27 | | prop 6457 |
. . . . . . . . . . . 12
⊢ (g ∈
P → ⟨(1^{st} ‘g), (2^{nd} ‘g)⟩ ∈
P) |
28 | | elprnql 6463 |
. . . . . . . . . . . 12
⊢
((⟨(1^{st} ‘g),
(2^{nd} ‘g)⟩ ∈ P ∧ z ∈ (1^{st} ‘g)) → z
∈ Q) |
29 | 27, 28 | sylan 267 |
. . . . . . . . . . 11
⊢
((g ∈ P ∧ z ∈ (1^{st} ‘g)) → z
∈ Q) |
30 | | genp.2 |
. . . . . . . . . . . 12
⊢
((y ∈ Q ∧ z ∈ Q) → (y𝐺z) ∈ Q) |
31 | | eleq1 2097 |
. . . . . . . . . . . 12
⊢ (x = (y𝐺z) → (x
∈ Q ↔ (y𝐺z) ∈ Q)) |
32 | 30, 31 | syl5ibrcom 146 |
. . . . . . . . . . 11
⊢
((y ∈ Q ∧ z ∈ Q) → (x = (y𝐺z) → x
∈ Q)) |
33 | 26, 29, 32 | syl2an 273 |
. . . . . . . . . 10
⊢
(((f ∈ P ∧ y ∈ (1^{st} ‘f)) ∧ (g ∈
P ∧ z ∈
(1^{st} ‘g))) →
(x = (y𝐺z)
→ x ∈ Q)) |
34 | 33 | an4s 522 |
. . . . . . . . 9
⊢
(((f ∈ P ∧ g ∈ P) ∧ (y ∈ (1^{st} ‘f) ∧ z ∈
(1^{st} ‘g))) →
(x = (y𝐺z)
→ x ∈ Q)) |
35 | 34 | rexlimdvva 2434 |
. . . . . . . 8
⊢
((f ∈ P ∧ g ∈ P) → (∃y ∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘g)x = (y𝐺z) → x
∈ Q)) |
36 | 35 | abssdv 3008 |
. . . . . . 7
⊢
((f ∈ P ∧ g ∈ P) → {x ∣ ∃y ∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘g)x = (y𝐺z)} ⊆ Q) |
37 | 23, 36 | syl5ss 2950 |
. . . . . 6
⊢
((f ∈ P ∧ g ∈ P) → {x ∈
Q ∣ ∃y ∈
(1^{st} ‘f)∃z ∈ (1^{st} ‘g)x = (y𝐺z)}
⊆ Q) |
38 | 22, 37 | ssexd 3888 |
. . . . 5
⊢
((f ∈ P ∧ g ∈ P) → {x ∈
Q ∣ ∃y ∈
(1^{st} ‘f)∃z ∈ (1^{st} ‘g)x = (y𝐺z)}
∈ V) |
39 | | rabssab 3021 |
. . . . . . 7
⊢ {x ∈
Q ∣ ∃y ∈
(2^{nd} ‘f)∃z ∈ (2^{nd} ‘g)x = (y𝐺z)}
⊆ {x ∣ ∃y ∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘g)x = (y𝐺z)} |
40 | | elprnqu 6464 |
. . . . . . . . . . . 12
⊢
((⟨(1^{st} ‘f),
(2^{nd} ‘f)⟩ ∈ P ∧ y ∈ (2^{nd} ‘f)) → y
∈ Q) |
41 | 24, 40 | sylan 267 |
. . . . . . . . . . 11
⊢
((f ∈ P ∧ y ∈ (2^{nd} ‘f)) → y
∈ Q) |
42 | | elprnqu 6464 |
. . . . . . . . . . . 12
⊢
((⟨(1^{st} ‘g),
(2^{nd} ‘g)⟩ ∈ P ∧ z ∈ (2^{nd} ‘g)) → z
∈ Q) |
43 | 27, 42 | sylan 267 |
. . . . . . . . . . 11
⊢
((g ∈ P ∧ z ∈ (2^{nd} ‘g)) → z
∈ Q) |
44 | 41, 43, 32 | syl2an 273 |
. . . . . . . . . 10
⊢
(((f ∈ P ∧ y ∈ (2^{nd} ‘f)) ∧ (g ∈
P ∧ z ∈
(2^{nd} ‘g))) →
(x = (y𝐺z)
→ x ∈ Q)) |
45 | 44 | an4s 522 |
. . . . . . . . 9
⊢
(((f ∈ P ∧ g ∈ P) ∧ (y ∈ (2^{nd} ‘f) ∧ z ∈
(2^{nd} ‘g))) →
(x = (y𝐺z)
→ x ∈ Q)) |
46 | 45 | rexlimdvva 2434 |
. . . . . . . 8
⊢
((f ∈ P ∧ g ∈ P) → (∃y ∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘g)x = (y𝐺z) → x
∈ Q)) |
47 | 46 | abssdv 3008 |
. . . . . . 7
⊢
((f ∈ P ∧ g ∈ P) → {x ∣ ∃y ∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘g)x = (y𝐺z)} ⊆ Q) |
48 | 39, 47 | syl5ss 2950 |
. . . . . 6
⊢
((f ∈ P ∧ g ∈ P) → {x ∈
Q ∣ ∃y ∈
(2^{nd} ‘f)∃z ∈ (2^{nd} ‘g)x = (y𝐺z)}
⊆ Q) |
49 | 22, 48 | ssexd 3888 |
. . . . 5
⊢
((f ∈ P ∧ g ∈ P) → {x ∈
Q ∣ ∃y ∈
(2^{nd} ‘f)∃z ∈ (2^{nd} ‘g)x = (y𝐺z)}
∈ V) |
50 | | opelxp 4317 |
. . . . 5
⊢
(⟨{x ∈ Q ∣ ∃y ∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘g)x = (y𝐺z)}⟩ ∈ (V
× V) ↔ ({x ∈ Q ∣ ∃y ∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘g)x = (y𝐺z)} ∈ V ∧ {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘g)x = (y𝐺z)} ∈
V)) |
51 | 38, 49, 50 | sylanbrc 394 |
. . . 4
⊢
((f ∈ P ∧ g ∈ P) → ⟨{x ∈
Q ∣ ∃y ∈
(1^{st} ‘f)∃z ∈ (1^{st} ‘g)x = (y𝐺z)},
{x ∈
Q ∣ ∃y ∈
(2^{nd} ‘f)∃z ∈ (2^{nd} ‘g)x = (y𝐺z)}⟩ ∈ (V
× V)) |
52 | | fveq2 5121 |
. . . . . . . 8
⊢ (w = f →
(1^{st} ‘w) = (1^{st}
‘f)) |
53 | 52 | rexeqdv 2506 |
. . . . . . 7
⊢ (w = f →
(∃y
∈ (1^{st} ‘w)∃z ∈
(1^{st} ‘v)x = (y𝐺z) ↔ ∃y ∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘v)x = (y𝐺z))) |
54 | 53 | rabbidv 2543 |
. . . . . 6
⊢ (w = f →
{x ∈
Q ∣ ∃y ∈
(1^{st} ‘w)∃z ∈ (1^{st} ‘v)x = (y𝐺z)} =
{x ∈
Q ∣ ∃y ∈
(1^{st} ‘f)∃z ∈ (1^{st} ‘v)x = (y𝐺z)}) |
55 | | fveq2 5121 |
. . . . . . . 8
⊢ (w = f →
(2^{nd} ‘w) = (2^{nd}
‘f)) |
56 | 55 | rexeqdv 2506 |
. . . . . . 7
⊢ (w = f →
(∃y
∈ (2^{nd} ‘w)∃z ∈
(2^{nd} ‘v)x = (y𝐺z) ↔ ∃y ∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘v)x = (y𝐺z))) |
57 | 56 | rabbidv 2543 |
. . . . . 6
⊢ (w = f →
{x ∈
Q ∣ ∃y ∈
(2^{nd} ‘w)∃z ∈ (2^{nd} ‘v)x = (y𝐺z)} =
{x ∈
Q ∣ ∃y ∈
(2^{nd} ‘f)∃z ∈ (2^{nd} ‘v)x = (y𝐺z)}) |
58 | 54, 57 | opeq12d 3548 |
. . . . 5
⊢ (w = f →
⟨{x ∈ Q ∣ ∃y ∈ (1^{st} ‘w)∃z ∈
(1^{st} ‘v)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘w)∃z ∈
(2^{nd} ‘v)x = (y𝐺z)}⟩ = ⟨{x ∈
Q ∣ ∃y ∈
(1^{st} ‘f)∃z ∈ (1^{st} ‘v)x = (y𝐺z)},
{x ∈
Q ∣ ∃y ∈
(2^{nd} ‘f)∃z ∈ (2^{nd} ‘v)x = (y𝐺z)}⟩) |
59 | | fveq2 5121 |
. . . . . . . . 9
⊢ (v = g →
(1^{st} ‘v) = (1^{st}
‘g)) |
60 | 59 | rexeqdv 2506 |
. . . . . . . 8
⊢ (v = g →
(∃z
∈ (1^{st} ‘v)x = (y𝐺z)
↔ ∃z ∈
(1^{st} ‘g)x = (y𝐺z))) |
61 | 60 | rexbidv 2321 |
. . . . . . 7
⊢ (v = g →
(∃y
∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘v)x = (y𝐺z) ↔ ∃y ∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘g)x = (y𝐺z))) |
62 | 61 | rabbidv 2543 |
. . . . . 6
⊢ (v = g →
{x ∈
Q ∣ ∃y ∈
(1^{st} ‘f)∃z ∈ (1^{st} ‘v)x = (y𝐺z)} =
{x ∈
Q ∣ ∃y ∈
(1^{st} ‘f)∃z ∈ (1^{st} ‘g)x = (y𝐺z)}) |
63 | | fveq2 5121 |
. . . . . . . . 9
⊢ (v = g →
(2^{nd} ‘v) = (2^{nd}
‘g)) |
64 | 63 | rexeqdv 2506 |
. . . . . . . 8
⊢ (v = g →
(∃z
∈ (2^{nd} ‘v)x = (y𝐺z)
↔ ∃z ∈
(2^{nd} ‘g)x = (y𝐺z))) |
65 | 64 | rexbidv 2321 |
. . . . . . 7
⊢ (v = g →
(∃y
∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘v)x = (y𝐺z) ↔ ∃y ∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘g)x = (y𝐺z))) |
66 | 65 | rabbidv 2543 |
. . . . . 6
⊢ (v = g →
{x ∈
Q ∣ ∃y ∈
(2^{nd} ‘f)∃z ∈ (2^{nd} ‘v)x = (y𝐺z)} =
{x ∈
Q ∣ ∃y ∈
(2^{nd} ‘f)∃z ∈ (2^{nd} ‘g)x = (y𝐺z)}) |
67 | 62, 66 | opeq12d 3548 |
. . . . 5
⊢ (v = g →
⟨{x ∈ Q ∣ ∃y ∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘v)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘v)x = (y𝐺z)}⟩ = ⟨{x ∈
Q ∣ ∃y ∈
(1^{st} ‘f)∃z ∈ (1^{st} ‘g)x = (y𝐺z)},
{x ∈
Q ∣ ∃y ∈
(2^{nd} ‘f)∃z ∈ (2^{nd} ‘g)x = (y𝐺z)}⟩) |
68 | | genp.1 |
. . . . . 6
⊢ 𝐹 = (w ∈
P, v ∈ P ↦ ⟨{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (1^{st} ‘w) ∧ z ∈
(1^{st} ‘v) ∧ x = (y𝐺z))},
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (2^{nd} ‘w) ∧ z ∈
(2^{nd} ‘v) ∧ x = (y𝐺z))}⟩) |
69 | 68 | genpdf 6490 |
. . . . 5
⊢ 𝐹 = (w ∈
P, v ∈ P ↦ ⟨{x ∈
Q ∣ ∃y ∈
(1^{st} ‘w)∃z ∈ (1^{st} ‘v)x = (y𝐺z)},
{x ∈
Q ∣ ∃y ∈
(2^{nd} ‘w)∃z ∈ (2^{nd} ‘v)x = (y𝐺z)}⟩) |
70 | 58, 67, 69 | ovmpt2g 5577 |
. . . 4
⊢
((f ∈ P ∧ g ∈ P ∧ ⟨{x ∈ Q ∣ ∃y ∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘g)x = (y𝐺z)}⟩ ∈ (V
× V)) → (f𝐹g) =
⟨{x ∈ Q ∣ ∃y ∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘g)x = (y𝐺z)}⟩) |
71 | 51, 70 | mpd3an3 1232 |
. . 3
⊢
((f ∈ P ∧ g ∈ P) → (f𝐹g) =
⟨{x ∈ Q ∣ ∃y ∈ (1^{st} ‘f)∃z ∈
(1^{st} ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘f)∃z ∈
(2^{nd} ‘g)x = (y𝐺z)}⟩) |
72 | 9, 20, 71 | vtocl2ga 2615 |
. 2
⊢
((A ∈ P ∧ B ∈ P) → (A𝐹B) =
⟨{x ∈ Q ∣ ∃y ∈ (1^{st} ‘A)∃z ∈
(1^{st} ‘B)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘A)∃z ∈
(2^{nd} ‘B)x = (y𝐺z)}⟩) |
73 | | eqeq1 2043 |
. . . . . 6
⊢ (x = 𝑞 → (x = (y𝐺z) ↔ 𝑞 = (y𝐺z))) |
74 | 73 | 2rexbidv 2343 |
. . . . 5
⊢ (x = 𝑞 → (∃y ∈ (1^{st} ‘A)∃z ∈
(1^{st} ‘B)x = (y𝐺z) ↔ ∃y ∈ (1^{st} ‘A)∃z ∈
(1^{st} ‘B)𝑞 = (y𝐺z))) |
75 | | oveq1 5462 |
. . . . . . 7
⊢ (y = 𝑟 → (y𝐺z) =
(𝑟𝐺z)) |
76 | 75 | eqeq2d 2048 |
. . . . . 6
⊢ (y = 𝑟 → (𝑞 = (y𝐺z)
↔ 𝑞 = (𝑟𝐺z))) |
77 | | oveq2 5463 |
. . . . . . 7
⊢ (z = 𝑠 → (𝑟𝐺z) =
(𝑟𝐺𝑠)) |
78 | 77 | eqeq2d 2048 |
. . . . . 6
⊢ (z = 𝑠 → (𝑞 = (𝑟𝐺z)
↔ 𝑞 = (𝑟𝐺𝑠))) |
79 | 76, 78 | cbvrex2v 2536 |
. . . . 5
⊢ (∃y ∈ (1^{st} ‘A)∃z ∈
(1^{st} ‘B)𝑞 = (y𝐺z)
↔ ∃𝑟 ∈
(1^{st} ‘A)∃𝑠 ∈
(1^{st} ‘B)𝑞 = (𝑟𝐺𝑠)) |
80 | 74, 79 | syl6bb 185 |
. . . 4
⊢ (x = 𝑞 → (∃y ∈ (1^{st} ‘A)∃z ∈
(1^{st} ‘B)x = (y𝐺z) ↔ ∃𝑟 ∈ (1^{st} ‘A)∃𝑠 ∈ (1^{st} ‘B)𝑞
= (𝑟𝐺𝑠))) |
81 | 80 | cbvrabv 2550 |
. . 3
⊢ {x ∈
Q ∣ ∃y ∈
(1^{st} ‘A)∃z ∈ (1^{st} ‘B)x = (y𝐺z)} =
{𝑞 ∈ Q ∣ ∃𝑟 ∈
(1^{st} ‘A)∃𝑠 ∈
(1^{st} ‘B)𝑞 = (𝑟𝐺𝑠)} |
82 | 73 | 2rexbidv 2343 |
. . . . 5
⊢ (x = 𝑞 → (∃y ∈ (2^{nd} ‘A)∃z ∈
(2^{nd} ‘B)x = (y𝐺z) ↔ ∃y ∈ (2^{nd} ‘A)∃z ∈
(2^{nd} ‘B)𝑞 = (y𝐺z))) |
83 | 76, 78 | cbvrex2v 2536 |
. . . . 5
⊢ (∃y ∈ (2^{nd} ‘A)∃z ∈
(2^{nd} ‘B)𝑞 = (y𝐺z)
↔ ∃𝑟 ∈
(2^{nd} ‘A)∃𝑠 ∈
(2^{nd} ‘B)𝑞 = (𝑟𝐺𝑠)) |
84 | 82, 83 | syl6bb 185 |
. . . 4
⊢ (x = 𝑞 → (∃y ∈ (2^{nd} ‘A)∃z ∈
(2^{nd} ‘B)x = (y𝐺z) ↔ ∃𝑟 ∈ (2^{nd} ‘A)∃𝑠 ∈ (2^{nd} ‘B)𝑞
= (𝑟𝐺𝑠))) |
85 | 84 | cbvrabv 2550 |
. . 3
⊢ {x ∈
Q ∣ ∃y ∈
(2^{nd} ‘A)∃z ∈ (2^{nd} ‘B)x = (y𝐺z)} =
{𝑞 ∈ Q ∣ ∃𝑟 ∈
(2^{nd} ‘A)∃𝑠 ∈
(2^{nd} ‘B)𝑞 = (𝑟𝐺𝑠)} |
86 | 81, 85 | opeq12i 3545 |
. 2
⊢
⟨{x ∈ Q ∣ ∃y ∈ (1^{st} ‘A)∃z ∈
(1^{st} ‘B)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^{nd} ‘A)∃z ∈
(2^{nd} ‘B)x = (y𝐺z)}⟩ = ⟨{𝑞 ∈
Q ∣ ∃𝑟 ∈
(1^{st} ‘A)∃𝑠 ∈
(1^{st} ‘B)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈
Q ∣ ∃𝑟 ∈
(2^{nd} ‘A)∃𝑠 ∈
(2^{nd} ‘B)𝑞 = (𝑟𝐺𝑠)}⟩ |
87 | 72, 86 | syl6eq 2085 |
1
⊢
((A ∈ P ∧ B ∈ P) → (A𝐹B) =
⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈
(1^{st} ‘A)∃𝑠 ∈
(1^{st} ‘B)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈
Q ∣ ∃𝑟 ∈
(2^{nd} ‘A)∃𝑠 ∈
(2^{nd} ‘B)𝑞 = (𝑟𝐺𝑠)}⟩) |