Step | Hyp | Ref
| Expression |
1 | | ffn 5319 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
2 | | dff1o4 5422 |
. . . . . 6
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵)) |
3 | 2 | baib 905 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ◡𝐹 Fn 𝐵)) |
4 | 1, 3 | syl 14 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ◡𝐹 Fn 𝐵)) |
5 | | fnres 5286 |
. . . . . 6
⊢ ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑧 𝑦◡𝐹𝑧) |
6 | | nfcv 2299 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑧 |
7 | | fmpt.1 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) |
8 | | nfmpt1 4057 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐶) |
9 | 7, 8 | nfcxfr 2296 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐹 |
10 | | nfcv 2299 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑦 |
11 | 6, 9, 10 | nfbr 4010 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑧𝐹𝑦 |
12 | | nfv 1508 |
. . . . . . . . 9
⊢
Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) |
13 | | breq1 3968 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑧𝐹𝑦 ↔ 𝑥𝐹𝑦)) |
14 | | df-mpt 4027 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} |
15 | 7, 14 | eqtri 2178 |
. . . . . . . . . . . 12
⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} |
16 | 15 | breqi 3971 |
. . . . . . . . . . 11
⊢ (𝑥𝐹𝑦 ↔ 𝑥{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦) |
17 | | df-br 3966 |
. . . . . . . . . . . 12
⊢ (𝑥{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}) |
18 | | opabid 4217 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)) |
19 | 17, 18 | bitri 183 |
. . . . . . . . . . 11
⊢ (𝑥{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)) |
20 | 16, 19 | bitri 183 |
. . . . . . . . . 10
⊢ (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)) |
21 | 13, 20 | bitrdi 195 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → (𝑧𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))) |
22 | 11, 12, 21 | cbveu 2030 |
. . . . . . . 8
⊢
(∃!𝑧 𝑧𝐹𝑦 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)) |
23 | | vex 2715 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
24 | | vex 2715 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
25 | 23, 24 | brcnv 4769 |
. . . . . . . . 9
⊢ (𝑦◡𝐹𝑧 ↔ 𝑧𝐹𝑦) |
26 | 25 | eubii 2015 |
. . . . . . . 8
⊢
(∃!𝑧 𝑦◡𝐹𝑧 ↔ ∃!𝑧 𝑧𝐹𝑦) |
27 | | df-reu 2442 |
. . . . . . . 8
⊢
(∃!𝑥 ∈
𝐴 𝑦 = 𝐶 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)) |
28 | 22, 26, 27 | 3bitr4i 211 |
. . . . . . 7
⊢
(∃!𝑧 𝑦◡𝐹𝑧 ↔ ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶) |
29 | 28 | ralbii 2463 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐵 ∃!𝑧 𝑦◡𝐹𝑧 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶) |
30 | 5, 29 | bitri 183 |
. . . . 5
⊢ ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶) |
31 | | relcnv 4964 |
. . . . . . 7
⊢ Rel ◡𝐹 |
32 | | df-rn 4597 |
. . . . . . . 8
⊢ ran 𝐹 = dom ◡𝐹 |
33 | | frn 5328 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵) |
34 | 32, 33 | eqsstrrid 3175 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → dom ◡𝐹 ⊆ 𝐵) |
35 | | relssres 4904 |
. . . . . . 7
⊢ ((Rel
◡𝐹 ∧ dom ◡𝐹 ⊆ 𝐵) → (◡𝐹 ↾ 𝐵) = ◡𝐹) |
36 | 31, 34, 35 | sylancr 411 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 ↾ 𝐵) = ◡𝐹) |
37 | 36 | fneq1d 5260 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ◡𝐹 Fn 𝐵)) |
38 | 30, 37 | bitr3id 193 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → (∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶 ↔ ◡𝐹 Fn 𝐵)) |
39 | 4, 38 | bitr4d 190 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)) |
40 | 39 | pm5.32i 450 |
. 2
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴–1-1-onto→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)) |
41 | | f1of 5414 |
. . 3
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) |
42 | 41 | pm4.71ri 390 |
. 2
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴–1-1-onto→𝐵)) |
43 | 7 | fmpt 5617 |
. . 3
⊢
(∀𝑥 ∈
𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
44 | 43 | anbi1i 454 |
. 2
⊢
((∀𝑥 ∈
𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)) |
45 | 40, 42, 44 | 3bitr4i 211 |
1
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)) |