Proof of Theorem ov
Step | Hyp | Ref
| Expression |
1 | | df-ov 7238 |
. . . . 5
⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) |
2 | | ov.6 |
. . . . . 6
⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} |
3 | 2 | fveq1i 6740 |
. . . . 5
⊢ (𝐹‘〈𝐴, 𝐵〉) = ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) |
4 | 1, 3 | eqtri 2767 |
. . . 4
⊢ (𝐴𝐹𝐵) = ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) |
5 | 4 | eqeq1i 2744 |
. . 3
⊢ ((𝐴𝐹𝐵) = 𝐶 ↔ ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝐶) |
6 | | ov.5 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃!𝑧𝜑) |
7 | 6 | fnoprab 7358 |
. . . . 5
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} Fn {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)} |
8 | | eleq1 2827 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑅 ↔ 𝐴 ∈ 𝑅)) |
9 | 8 | anbi1d 633 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ↔ (𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆))) |
10 | | eleq1 2827 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝑦 ∈ 𝑆 ↔ 𝐵 ∈ 𝑆)) |
11 | 10 | anbi2d 632 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → ((𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ↔ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆))) |
12 | 9, 11 | opelopabg 5436 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)} ↔ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆))) |
13 | 12 | ibir 271 |
. . . . 5
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)}) |
14 | | fnopfvb 6788 |
. . . . 5
⊢
(({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} Fn {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)} ∧ 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)}) → (({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝐶 ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)})) |
15 | 7, 13, 14 | sylancr 590 |
. . . 4
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝐶 ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)})) |
16 | | ov.1 |
. . . . 5
⊢ 𝐶 ∈ V |
17 | | ov.2 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
18 | 9, 17 | anbi12d 634 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑) ↔ ((𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜓))) |
19 | | ov.3 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) |
20 | 11, 19 | anbi12d 634 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (((𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜓) ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜒))) |
21 | | ov.4 |
. . . . . . 7
⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) |
22 | 21 | anbi2d 632 |
. . . . . 6
⊢ (𝑧 = 𝐶 → (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜒) ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃))) |
23 | 18, 20, 22 | eloprabg 7342 |
. . . . 5
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ V) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃))) |
24 | 16, 23 | mp3an3 1452 |
. . . 4
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃))) |
25 | 15, 24 | bitrd 282 |
. . 3
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝐶 ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃))) |
26 | 5, 25 | syl5bb 286 |
. 2
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵) = 𝐶 ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃))) |
27 | 26 | bianabs 545 |
1
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵) = 𝐶 ↔ 𝜃)) |