| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ffn 6735 | . . . . 5
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | 
| 2 |  | dff1o4 6855 | . . . . . 6
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵)) | 
| 3 | 2 | baib 535 | . . . . 5
⊢ (𝐹 Fn 𝐴 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ◡𝐹 Fn 𝐵)) | 
| 4 | 1, 3 | syl 17 | . . . 4
⊢ (𝐹:𝐴⟶𝐵 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ◡𝐹 Fn 𝐵)) | 
| 5 |  | fnres 6694 | . . . . . 6
⊢ ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑧 𝑦◡𝐹𝑧) | 
| 6 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑥𝑧 | 
| 7 |  | fmpt.1 | . . . . . . . . . . 11
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) | 
| 8 |  | nfmpt1 5249 | . . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐶) | 
| 9 | 7, 8 | nfcxfr 2902 | . . . . . . . . . 10
⊢
Ⅎ𝑥𝐹 | 
| 10 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑥𝑦 | 
| 11 | 6, 9, 10 | nfbr 5189 | . . . . . . . . 9
⊢
Ⅎ𝑥 𝑧𝐹𝑦 | 
| 12 |  | nfv 1913 | . . . . . . . . 9
⊢
Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) | 
| 13 |  | breq1 5145 | . . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑧𝐹𝑦 ↔ 𝑥𝐹𝑦)) | 
| 14 |  | df-mpt 5225 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} | 
| 15 | 7, 14 | eqtri 2764 | . . . . . . . . . . . 12
⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} | 
| 16 | 15 | breqi 5148 | . . . . . . . . . . 11
⊢ (𝑥𝐹𝑦 ↔ 𝑥{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦) | 
| 17 |  | df-br 5143 | . . . . . . . . . . . 12
⊢ (𝑥{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}) | 
| 18 |  | opabidw 5528 | . . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)) | 
| 19 | 17, 18 | bitri 275 | . . . . . . . . . . 11
⊢ (𝑥{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)) | 
| 20 | 16, 19 | bitri 275 | . . . . . . . . . 10
⊢ (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)) | 
| 21 | 13, 20 | bitrdi 287 | . . . . . . . . 9
⊢ (𝑧 = 𝑥 → (𝑧𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))) | 
| 22 | 11, 12, 21 | cbveuw 2605 | . . . . . . . 8
⊢
(∃!𝑧 𝑧𝐹𝑦 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)) | 
| 23 |  | vex 3483 | . . . . . . . . . 10
⊢ 𝑦 ∈ V | 
| 24 |  | vex 3483 | . . . . . . . . . 10
⊢ 𝑧 ∈ V | 
| 25 | 23, 24 | brcnv 5892 | . . . . . . . . 9
⊢ (𝑦◡𝐹𝑧 ↔ 𝑧𝐹𝑦) | 
| 26 | 25 | eubii 2584 | . . . . . . . 8
⊢
(∃!𝑧 𝑦◡𝐹𝑧 ↔ ∃!𝑧 𝑧𝐹𝑦) | 
| 27 |  | df-reu 3380 | . . . . . . . 8
⊢
(∃!𝑥 ∈
𝐴 𝑦 = 𝐶 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)) | 
| 28 | 22, 26, 27 | 3bitr4i 303 | . . . . . . 7
⊢
(∃!𝑧 𝑦◡𝐹𝑧 ↔ ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶) | 
| 29 | 28 | ralbii 3092 | . . . . . 6
⊢
(∀𝑦 ∈
𝐵 ∃!𝑧 𝑦◡𝐹𝑧 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶) | 
| 30 | 5, 29 | bitri 275 | . . . . 5
⊢ ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶) | 
| 31 |  | relcnv 6121 | . . . . . . 7
⊢ Rel ◡𝐹 | 
| 32 |  | df-rn 5695 | . . . . . . . 8
⊢ ran 𝐹 = dom ◡𝐹 | 
| 33 |  | frn 6742 | . . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵) | 
| 34 | 32, 33 | eqsstrrid 4022 | . . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → dom ◡𝐹 ⊆ 𝐵) | 
| 35 |  | relssres 6039 | . . . . . . 7
⊢ ((Rel
◡𝐹 ∧ dom ◡𝐹 ⊆ 𝐵) → (◡𝐹 ↾ 𝐵) = ◡𝐹) | 
| 36 | 31, 34, 35 | sylancr 587 | . . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 ↾ 𝐵) = ◡𝐹) | 
| 37 | 36 | fneq1d 6660 | . . . . 5
⊢ (𝐹:𝐴⟶𝐵 → ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ◡𝐹 Fn 𝐵)) | 
| 38 | 30, 37 | bitr3id 285 | . . . 4
⊢ (𝐹:𝐴⟶𝐵 → (∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶 ↔ ◡𝐹 Fn 𝐵)) | 
| 39 | 4, 38 | bitr4d 282 | . . 3
⊢ (𝐹:𝐴⟶𝐵 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)) | 
| 40 | 39 | pm5.32i 574 | . 2
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴–1-1-onto→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)) | 
| 41 |  | f1of 6847 | . . 3
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) | 
| 42 | 41 | pm4.71ri 560 | . 2
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴–1-1-onto→𝐵)) | 
| 43 | 7 | fmpt 7129 | . . 3
⊢
(∀𝑥 ∈
𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) | 
| 44 | 43 | anbi1i 624 | . 2
⊢
((∀𝑥 ∈
𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)) | 
| 45 | 40, 42, 44 | 3bitr4i 303 | 1
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)) |