Step | Hyp | Ref
| Expression |
1 | | relcnv 6057 |
. 2
⊢ Rel ◡(𝐹 ↾ 𝐴) |
2 | | relres 5967 |
. 2
⊢ Rel
(◡𝐹 ↾ 𝐵) |
3 | | opelf 6704 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
4 | 3 | simpld 496 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹) → 𝑥 ∈ 𝐴) |
5 | 4 | ex 414 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → 𝑥 ∈ 𝐴)) |
6 | 5 | pm4.71rd 564 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ↔ (𝑥 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹))) |
7 | | vex 3450 |
. . . . . 6
⊢ 𝑦 ∈ V |
8 | | vex 3450 |
. . . . . 6
⊢ 𝑥 ∈ V |
9 | 7, 8 | opelcnv 5838 |
. . . . 5
⊢
(⟨𝑦, 𝑥⟩ ∈ ◡(𝐹 ↾ 𝐴) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐹 ↾ 𝐴)) |
10 | 7 | opelresi 5946 |
. . . . 5
⊢
(⟨𝑥, 𝑦⟩ ∈ (𝐹 ↾ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹)) |
11 | 9, 10 | bitri 275 |
. . . 4
⊢
(⟨𝑦, 𝑥⟩ ∈ ◡(𝐹 ↾ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹)) |
12 | 6, 11 | bitr4di 289 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡(𝐹 ↾ 𝐴))) |
13 | 3 | simprd 497 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹) → 𝑦 ∈ 𝐵) |
14 | 13 | ex 414 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → 𝑦 ∈ 𝐵)) |
15 | 14 | pm4.71rd 564 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹))) |
16 | 8 | opelresi 5946 |
. . . . 5
⊢
(⟨𝑦, 𝑥⟩ ∈ (◡𝐹 ↾ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ ◡𝐹)) |
17 | 7, 8 | opelcnv 5838 |
. . . . . 6
⊢
(⟨𝑦, 𝑥⟩ ∈ ◡𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹) |
18 | 17 | anbi2i 624 |
. . . . 5
⊢ ((𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ ◡𝐹) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹)) |
19 | 16, 18 | bitri 275 |
. . . 4
⊢
(⟨𝑦, 𝑥⟩ ∈ (◡𝐹 ↾ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹)) |
20 | 15, 19 | bitr4di 289 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ↔ ⟨𝑦, 𝑥⟩ ∈ (◡𝐹 ↾ 𝐵))) |
21 | 12, 20 | bitr3d 281 |
. 2
⊢ (𝐹:𝐴⟶𝐵 → (⟨𝑦, 𝑥⟩ ∈ ◡(𝐹 ↾ 𝐴) ↔ ⟨𝑦, 𝑥⟩ ∈ (◡𝐹 ↾ 𝐵))) |
22 | 1, 2, 21 | eqrelrdv 5749 |
1
⊢ (𝐹:𝐴⟶𝐵 → ◡(𝐹 ↾ 𝐴) = (◡𝐹 ↾ 𝐵)) |