Proof of Theorem fgraphopab
Step | Hyp | Ref
| Expression |
1 | | fssxp 6310 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵)) |
2 | | df-ss 3806 |
. . . 4
⊢ (𝐹 ⊆ (𝐴 × 𝐵) ↔ (𝐹 ∩ (𝐴 × 𝐵)) = 𝐹) |
3 | 1, 2 | sylib 210 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ∩ (𝐴 × 𝐵)) = 𝐹) |
4 | | ffn 6291 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
5 | | dffn5 6501 |
. . . . 5
⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎))) |
6 | 4, 5 | sylib 210 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎))) |
7 | 6 | ineq1d 4036 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ∩ (𝐴 × 𝐵)) = ((𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎)) ∩ (𝐴 × 𝐵))) |
8 | 3, 7 | eqtr3d 2816 |
. 2
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = ((𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎)) ∩ (𝐴 × 𝐵))) |
9 | | df-mpt 4966 |
. . . 4
⊢ (𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎)) = {〈𝑎, 𝑏〉 ∣ (𝑎 ∈ 𝐴 ∧ 𝑏 = (𝐹‘𝑎))} |
10 | | df-xp 5361 |
. . . 4
⊢ (𝐴 × 𝐵) = {〈𝑎, 𝑏〉 ∣ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)} |
11 | 9, 10 | ineq12i 4035 |
. . 3
⊢ ((𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎)) ∩ (𝐴 × 𝐵)) = ({〈𝑎, 𝑏〉 ∣ (𝑎 ∈ 𝐴 ∧ 𝑏 = (𝐹‘𝑎))} ∩ {〈𝑎, 𝑏〉 ∣ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)}) |
12 | | inopab 5498 |
. . 3
⊢
({〈𝑎, 𝑏〉 ∣ (𝑎 ∈ 𝐴 ∧ 𝑏 = (𝐹‘𝑎))} ∩ {〈𝑎, 𝑏〉 ∣ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)}) = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 = (𝐹‘𝑎)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵))} |
13 | | anandi 666 |
. . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ (𝑏 = (𝐹‘𝑎) ∧ 𝑏 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 = (𝐹‘𝑎)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵))) |
14 | | ancom 454 |
. . . . . . 7
⊢ ((𝑏 = (𝐹‘𝑎) ∧ 𝑏 ∈ 𝐵) ↔ (𝑏 ∈ 𝐵 ∧ 𝑏 = (𝐹‘𝑎))) |
15 | 14 | anbi2i 616 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ (𝑏 = (𝐹‘𝑎) ∧ 𝑏 ∈ 𝐵)) ↔ (𝑎 ∈ 𝐴 ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 = (𝐹‘𝑎)))) |
16 | | anass 462 |
. . . . . 6
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 = (𝐹‘𝑎)) ↔ (𝑎 ∈ 𝐴 ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 = (𝐹‘𝑎)))) |
17 | | eqcom 2785 |
. . . . . . 7
⊢ (𝑏 = (𝐹‘𝑎) ↔ (𝐹‘𝑎) = 𝑏) |
18 | 17 | anbi2i 616 |
. . . . . 6
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 = (𝐹‘𝑎)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)) |
19 | 15, 16, 18 | 3bitr2i 291 |
. . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ (𝑏 = (𝐹‘𝑎) ∧ 𝑏 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)) |
20 | 13, 19 | bitr3i 269 |
. . . 4
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 = (𝐹‘𝑎)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)) |
21 | 20 | opabbii 4953 |
. . 3
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 = (𝐹‘𝑎)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)} |
22 | 11, 12, 21 | 3eqtri 2806 |
. 2
⊢ ((𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎)) ∩ (𝐴 × 𝐵)) = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)} |
23 | 8, 22 | syl6eq 2830 |
1
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)}) |