Proof of Theorem ov
Step | Hyp | Ref
| Expression |
1 | | df-ov 5458 |
. . . . 5
⊢ (A𝐹B) =
(𝐹‘〈A, B〉) |
2 | | ov.6 |
. . . . . 6
⊢ 𝐹 = {〈〈x, y〉,
z〉 ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)} |
3 | 2 | fveq1i 5122 |
. . . . 5
⊢ (𝐹‘〈A, B〉) =
({〈〈x, y〉, z〉
∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)}‘〈A, B〉) |
4 | 1, 3 | eqtri 2057 |
. . . 4
⊢ (A𝐹B) =
({〈〈x, y〉, z〉
∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)}‘〈A, B〉) |
5 | 4 | eqeq1i 2044 |
. . 3
⊢
((A𝐹B) =
𝐶 ↔
({〈〈x, y〉, z〉
∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)}‘〈A, B〉) =
𝐶) |
6 | | ov.5 |
. . . . . 6
⊢
((x ∈ 𝑅 ∧ y ∈ 𝑆) → ∃!zφ) |
7 | 6 | fnoprab 5546 |
. . . . 5
⊢
{〈〈x, y〉, z〉
∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)} Fn
{〈x, y〉 ∣ (x ∈ 𝑅 ∧ y ∈ 𝑆)} |
8 | | eleq1 2097 |
. . . . . . . 8
⊢ (x = A →
(x ∈
𝑅 ↔ A ∈ 𝑅)) |
9 | 8 | anbi1d 438 |
. . . . . . 7
⊢ (x = A →
((x ∈
𝑅 ∧ y ∈ 𝑆) ↔ (A ∈ 𝑅 ∧ y ∈ 𝑆))) |
10 | | eleq1 2097 |
. . . . . . . 8
⊢ (y = B →
(y ∈
𝑆 ↔ B ∈ 𝑆)) |
11 | 10 | anbi2d 437 |
. . . . . . 7
⊢ (y = B →
((A ∈
𝑅 ∧ y ∈ 𝑆) ↔ (A ∈ 𝑅 ∧ B ∈ 𝑆))) |
12 | 9, 11 | opelopabg 3996 |
. . . . . 6
⊢
((A ∈ 𝑅 ∧ B ∈ 𝑆) → (〈A, B〉 ∈ {〈x,
y〉 ∣ (x ∈ 𝑅 ∧ y ∈ 𝑆)} ↔ (A ∈ 𝑅 ∧ B ∈ 𝑆))) |
13 | 12 | ibir 166 |
. . . . 5
⊢
((A ∈ 𝑅 ∧ B ∈ 𝑆) → 〈A, B〉 ∈ {〈x,
y〉 ∣ (x ∈ 𝑅 ∧ y ∈ 𝑆)}) |
14 | | fnopfvb 5158 |
. . . . 5
⊢
(({〈〈x, y〉, z〉
∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)} Fn
{〈x, y〉 ∣ (x ∈ 𝑅 ∧ y ∈ 𝑆)} ∧
〈A, B〉 ∈
{〈x, y〉 ∣ (x ∈ 𝑅 ∧ y ∈ 𝑆)}) → (({〈〈x, y〉,
z〉 ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)}‘〈A, B〉) =
𝐶 ↔
〈〈A, B〉, 𝐶〉 ∈
{〈〈x, y〉, z〉
∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)})) |
15 | 7, 13, 14 | sylancr 393 |
. . . 4
⊢
((A ∈ 𝑅 ∧ B ∈ 𝑆) → (({〈〈x, y〉,
z〉 ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)}‘〈A, B〉) =
𝐶 ↔
〈〈A, B〉, 𝐶〉 ∈
{〈〈x, y〉, z〉
∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)})) |
16 | | ov.1 |
. . . . 5
⊢ 𝐶 ∈ V |
17 | | ov.2 |
. . . . . . 7
⊢ (x = A →
(φ ↔ ψ)) |
18 | 9, 17 | anbi12d 442 |
. . . . . 6
⊢ (x = A →
(((x ∈
𝑅 ∧ y ∈ 𝑆) ∧ φ) ↔ ((A ∈ 𝑅 ∧ y ∈ 𝑆) ∧ ψ))) |
19 | | ov.3 |
. . . . . . 7
⊢ (y = B →
(ψ ↔ χ)) |
20 | 11, 19 | anbi12d 442 |
. . . . . 6
⊢ (y = B →
(((A ∈
𝑅 ∧ y ∈ 𝑆) ∧ ψ) ↔ ((A ∈ 𝑅 ∧ B ∈ 𝑆) ∧ χ))) |
21 | | ov.4 |
. . . . . . 7
⊢ (z = 𝐶 → (χ ↔ θ)) |
22 | 21 | anbi2d 437 |
. . . . . 6
⊢ (z = 𝐶 → (((A ∈ 𝑅 ∧ B ∈ 𝑆) ∧ χ) ↔ ((A ∈ 𝑅 ∧ B ∈ 𝑆) ∧ θ))) |
23 | 18, 20, 22 | eloprabg 5534 |
. . . . 5
⊢
((A ∈ 𝑅 ∧ B ∈ 𝑆 ∧ 𝐶 ∈ V)
→ (〈〈A, B〉, 𝐶〉 ∈
{〈〈x, y〉, z〉
∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)} ↔
((A ∈
𝑅 ∧ B ∈ 𝑆) ∧ θ))) |
24 | 16, 23 | mp3an3 1220 |
. . . 4
⊢
((A ∈ 𝑅 ∧ B ∈ 𝑆) → (〈〈A, B〉,
𝐶〉 ∈ {〈〈x, y〉,
z〉 ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)} ↔ ((A ∈ 𝑅 ∧ B ∈ 𝑆) ∧ θ))) |
25 | 15, 24 | bitrd 177 |
. . 3
⊢
((A ∈ 𝑅 ∧ B ∈ 𝑆) → (({〈〈x, y〉,
z〉 ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)}‘〈A, B〉) =
𝐶 ↔ ((A ∈ 𝑅 ∧ B ∈ 𝑆) ∧ θ))) |
26 | 5, 25 | syl5bb 181 |
. 2
⊢
((A ∈ 𝑅 ∧ B ∈ 𝑆) → ((A𝐹B) =
𝐶 ↔ ((A ∈ 𝑅 ∧ B ∈ 𝑆) ∧ θ))) |
27 | 26 | bianabs 543 |
1
⊢
((A ∈ 𝑅 ∧ B ∈ 𝑆) → ((A𝐹B) =
𝐶 ↔ θ)) |