Step | Hyp | Ref
| Expression |
1 | | df-ov 5526 |
. 2
⊢ (AFB) = (F
‘〈A, B〉) |
2 | | eqid 2353 |
. . . . . 6
⊢ S = S |
3 | | biidd 228 |
. . . . . . 7
⊢ ((x = A ∧ y = B) → (S =
S ↔ S = S)) |
4 | 3 | copsex2g 4609 |
. . . . . 6
⊢ ((A ∈ G ∧ B ∈ H) → (∃x∃y(〈A, B〉 = 〈x, y〉 ∧ S = S) ↔ S =
S)) |
5 | 2, 4 | mpbiri 224 |
. . . . 5
⊢ ((A ∈ G ∧ B ∈ H) → ∃x∃y(〈A, B〉 = 〈x, y〉 ∧ S = S)) |
6 | 5 | 3adant3 975 |
. . . 4
⊢ ((A ∈ G ∧ B ∈ H ∧ 〈A, B〉 ∈ C) →
∃x∃y(〈A, B〉 = 〈x, y〉 ∧ S = S)) |
7 | 6 | adantr 451 |
. . 3
⊢ (((A ∈ G ∧ B ∈ H ∧ 〈A, B〉 ∈ C) ∧ S ∈ J) →
∃x∃y(〈A, B〉 = 〈x, y〉 ∧ S = S)) |
8 | | eqeq1 2359 |
. . . . . . . 8
⊢ (w = 〈A, B〉 → (w =
〈x,
y〉 ↔
〈A,
B〉 =
〈x,
y〉)) |
9 | 8 | anbi1d 685 |
. . . . . . 7
⊢ (w = 〈A, B〉 → ((w =
〈x,
y〉 ∧ z = R) ↔ (〈A, B〉 = 〈x, y〉 ∧ z = R))) |
10 | | ov6g.1 |
. . . . . . . . . 10
⊢ (〈x, y〉 = 〈A, B〉 → R = S) |
11 | 10 | eqeq2d 2364 |
. . . . . . . . 9
⊢ (〈x, y〉 = 〈A, B〉 →
(z = R
↔ z = S)) |
12 | 11 | eqcoms 2356 |
. . . . . . . 8
⊢ (〈A, B〉 = 〈x, y〉 →
(z = R
↔ z = S)) |
13 | 12 | pm5.32i 618 |
. . . . . . 7
⊢ ((〈A, B〉 = 〈x, y〉 ∧ z = R) ↔ (〈A, B〉 = 〈x, y〉 ∧ z = S)) |
14 | 9, 13 | syl6bb 252 |
. . . . . 6
⊢ (w = 〈A, B〉 → ((w =
〈x,
y〉 ∧ z = R) ↔ (〈A, B〉 = 〈x, y〉 ∧ z = S))) |
15 | 14 | 2exbidv 1628 |
. . . . 5
⊢ (w = 〈A, B〉 → (∃x∃y(w = 〈x, y〉 ∧ z = R) ↔
∃x∃y(〈A, B〉 = 〈x, y〉 ∧ z = S))) |
16 | | eqeq1 2359 |
. . . . . . 7
⊢ (z = S →
(z = S
↔ S = S)) |
17 | 16 | anbi2d 684 |
. . . . . 6
⊢ (z = S →
((〈A,
B〉 =
〈x,
y〉 ∧ z = S) ↔ (〈A, B〉 = 〈x, y〉 ∧ S = S))) |
18 | 17 | 2exbidv 1628 |
. . . . 5
⊢ (z = S →
(∃x∃y(〈A, B〉 = 〈x, y〉 ∧ z = S) ↔ ∃x∃y(〈A, B〉 = 〈x, y〉 ∧ S = S))) |
19 | | moeq 3012 |
. . . . . . 7
⊢ ∃*z z = R |
20 | 19 | mosubop 4613 |
. . . . . 6
⊢ ∃*z∃x∃y(w = 〈x, y〉 ∧ z = R) |
21 | 20 | a1i 10 |
. . . . 5
⊢ (w ∈ C → ∃*z∃x∃y(w = 〈x, y〉 ∧ z = R)) |
22 | | ov6g.2 |
. . . . . 6
⊢ F = {〈〈x, y〉, z〉 ∣ (〈x, y〉 ∈ C ∧ z = R)} |
23 | | dfoprab2 5558 |
. . . . . 6
⊢ {〈〈x, y〉, z〉 ∣ (〈x, y〉 ∈ C ∧ z = R)} = {〈w, z〉 ∣ ∃x∃y(w = 〈x, y〉 ∧ (〈x, y〉 ∈ C ∧ z = R))} |
24 | | eleq1 2413 |
. . . . . . . . . . . 12
⊢ (w = 〈x, y〉 → (w
∈ C
↔ 〈x, y〉 ∈ C)) |
25 | 24 | anbi1d 685 |
. . . . . . . . . . 11
⊢ (w = 〈x, y〉 → ((w
∈ C ∧ z = R) ↔ (〈x, y〉 ∈ C ∧ z = R))) |
26 | 25 | pm5.32i 618 |
. . . . . . . . . 10
⊢ ((w = 〈x, y〉 ∧ (w ∈ C ∧ z = R)) ↔
(w = 〈x, y〉 ∧ (〈x, y〉 ∈ C ∧ z = R))) |
27 | | an12 772 |
. . . . . . . . . 10
⊢ ((w = 〈x, y〉 ∧ (w ∈ C ∧ z = R)) ↔
(w ∈
C ∧
(w = 〈x, y〉 ∧ z = R))) |
28 | 26, 27 | bitr3i 242 |
. . . . . . . . 9
⊢ ((w = 〈x, y〉 ∧ (〈x, y〉 ∈ C ∧ z = R)) ↔ (w
∈ C ∧ (w = 〈x, y〉 ∧ z = R))) |
29 | 28 | 2exbii 1583 |
. . . . . . . 8
⊢ (∃x∃y(w = 〈x, y〉 ∧ (〈x, y〉 ∈ C ∧ z = R)) ↔ ∃x∃y(w ∈ C ∧ (w = 〈x, y〉 ∧ z = R))) |
30 | | 19.42vv 1907 |
. . . . . . . 8
⊢ (∃x∃y(w ∈ C ∧ (w = 〈x, y〉 ∧ z = R)) ↔
(w ∈
C ∧ ∃x∃y(w = 〈x, y〉 ∧ z = R))) |
31 | 29, 30 | bitri 240 |
. . . . . . 7
⊢ (∃x∃y(w = 〈x, y〉 ∧ (〈x, y〉 ∈ C ∧ z = R)) ↔ (w
∈ C ∧ ∃x∃y(w = 〈x, y〉 ∧ z = R))) |
32 | 31 | opabbii 4626 |
. . . . . 6
⊢ {〈w, z〉 ∣ ∃x∃y(w = 〈x, y〉 ∧ (〈x, y〉 ∈ C ∧ z = R))} =
{〈w,
z〉 ∣ (w ∈ C ∧ ∃x∃y(w = 〈x, y〉 ∧ z = R))} |
33 | 22, 23, 32 | 3eqtri 2377 |
. . . . 5
⊢ F = {〈w, z〉 ∣ (w ∈ C ∧ ∃x∃y(w = 〈x, y〉 ∧ z = R))} |
34 | 15, 18, 21, 33 | fvopab3ig 5387 |
. . . 4
⊢ ((〈A, B〉 ∈ C ∧ S ∈ J) →
(∃x∃y(〈A, B〉 = 〈x, y〉 ∧ S = S) → (F
‘〈A, B〉) = S)) |
35 | 34 | 3ad2antl3 1119 |
. . 3
⊢ (((A ∈ G ∧ B ∈ H ∧ 〈A, B〉 ∈ C) ∧ S ∈ J) →
(∃x∃y(〈A, B〉 = 〈x, y〉 ∧ S = S) → (F
‘〈A, B〉) = S)) |
36 | 7, 35 | mpd 14 |
. 2
⊢ (((A ∈ G ∧ B ∈ H ∧ 〈A, B〉 ∈ C) ∧ S ∈ J) →
(F ‘〈A, B〉) = S) |
37 | 1, 36 | syl5eq 2397 |
1
⊢ (((A ∈ G ∧ B ∈ H ∧ 〈A, B〉 ∈ C) ∧ S ∈ J) →
(AFB) = S) |