Step | Hyp | Ref
| Expression |
1 | | fssxp 6701 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵)) |
2 | | df-ss 3932 |
. . . 4
⊢ (𝐹 ⊆ (𝐴 × 𝐵) ↔ (𝐹 ∩ (𝐴 × 𝐵)) = 𝐹) |
3 | 1, 2 | sylib 217 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ∩ (𝐴 × 𝐵)) = 𝐹) |
4 | | ffn 6673 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
5 | | dffn5 6906 |
. . . . 5
⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎))) |
6 | 4, 5 | sylib 217 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎))) |
7 | 6 | ineq1d 4176 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ∩ (𝐴 × 𝐵)) = ((𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎)) ∩ (𝐴 × 𝐵))) |
8 | 3, 7 | eqtr3d 2779 |
. 2
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = ((𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎)) ∩ (𝐴 × 𝐵))) |
9 | | df-mpt 5194 |
. . . 4
⊢ (𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎)) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝐴 ∧ 𝑏 = (𝐹‘𝑎))} |
10 | | df-xp 5644 |
. . . 4
⊢ (𝐴 × 𝐵) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)} |
11 | 9, 10 | ineq12i 4175 |
. . 3
⊢ ((𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎)) ∩ (𝐴 × 𝐵)) = ({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝐴 ∧ 𝑏 = (𝐹‘𝑎))} ∩ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)}) |
12 | | inopab 5790 |
. . 3
⊢
({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝐴 ∧ 𝑏 = (𝐹‘𝑎))} ∩ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)}) = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 = (𝐹‘𝑎)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵))} |
13 | | anandi 675 |
. . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ (𝑏 = (𝐹‘𝑎) ∧ 𝑏 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 = (𝐹‘𝑎)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵))) |
14 | | ancom 462 |
. . . . . . 7
⊢ ((𝑏 = (𝐹‘𝑎) ∧ 𝑏 ∈ 𝐵) ↔ (𝑏 ∈ 𝐵 ∧ 𝑏 = (𝐹‘𝑎))) |
15 | 14 | anbi2i 624 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ (𝑏 = (𝐹‘𝑎) ∧ 𝑏 ∈ 𝐵)) ↔ (𝑎 ∈ 𝐴 ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 = (𝐹‘𝑎)))) |
16 | | anass 470 |
. . . . . 6
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 = (𝐹‘𝑎)) ↔ (𝑎 ∈ 𝐴 ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 = (𝐹‘𝑎)))) |
17 | | eqcom 2744 |
. . . . . . 7
⊢ (𝑏 = (𝐹‘𝑎) ↔ (𝐹‘𝑎) = 𝑏) |
18 | 17 | anbi2i 624 |
. . . . . 6
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 = (𝐹‘𝑎)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)) |
19 | 15, 16, 18 | 3bitr2i 299 |
. . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ (𝑏 = (𝐹‘𝑎) ∧ 𝑏 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)) |
20 | 13, 19 | bitr3i 277 |
. . . 4
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 = (𝐹‘𝑎)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)) |
21 | 20 | opabbii 5177 |
. . 3
⊢
{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 = (𝐹‘𝑎)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)} |
22 | 11, 12, 21 | 3eqtri 2769 |
. 2
⊢ ((𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎)) ∩ (𝐴 × 𝐵)) = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)} |
23 | 8, 22 | eqtrdi 2793 |
1
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)}) |