Proof of Theorem mapsn
Step | Hyp | Ref
| Expression |
1 | | map0.1 |
. . . 4
⊢ 𝐴 ∈ V |
2 | | snex 4835 |
. . . 4
⊢ {𝐵} ∈ V |
3 | 1, 2 | elmap 7772 |
. . 3
⊢ (𝑓 ∈ (𝐴 ↑𝑚 {𝐵}) ↔ 𝑓:{𝐵}⟶𝐴) |
4 | | ffn 5958 |
. . . . . . . 8
⊢ (𝑓:{𝐵}⟶𝐴 → 𝑓 Fn {𝐵}) |
5 | | map0.2 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
6 | 5 | snid 4155 |
. . . . . . . 8
⊢ 𝐵 ∈ {𝐵} |
7 | | fneu 5909 |
. . . . . . . 8
⊢ ((𝑓 Fn {𝐵} ∧ 𝐵 ∈ {𝐵}) → ∃!𝑦 𝐵𝑓𝑦) |
8 | 4, 6, 7 | sylancl 693 |
. . . . . . 7
⊢ (𝑓:{𝐵}⟶𝐴 → ∃!𝑦 𝐵𝑓𝑦) |
9 | | euabsn 4205 |
. . . . . . . 8
⊢
(∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦{𝑦 ∣ 𝐵𝑓𝑦} = {𝑦}) |
10 | | frel 5963 |
. . . . . . . . . . . 12
⊢ (𝑓:{𝐵}⟶𝐴 → Rel 𝑓) |
11 | | relimasn 5407 |
. . . . . . . . . . . 12
⊢ (Rel
𝑓 → (𝑓 “ {𝐵}) = {𝑦 ∣ 𝐵𝑓𝑦}) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑓:{𝐵}⟶𝐴 → (𝑓 “ {𝐵}) = {𝑦 ∣ 𝐵𝑓𝑦}) |
13 | | imadmrn 5395 |
. . . . . . . . . . . 12
⊢ (𝑓 “ dom 𝑓) = ran 𝑓 |
14 | | fdm 5964 |
. . . . . . . . . . . . 13
⊢ (𝑓:{𝐵}⟶𝐴 → dom 𝑓 = {𝐵}) |
15 | 14 | imaeq2d 5385 |
. . . . . . . . . . . 12
⊢ (𝑓:{𝐵}⟶𝐴 → (𝑓 “ dom 𝑓) = (𝑓 “ {𝐵})) |
16 | 13, 15 | syl5reqr 2659 |
. . . . . . . . . . 11
⊢ (𝑓:{𝐵}⟶𝐴 → (𝑓 “ {𝐵}) = ran 𝑓) |
17 | 12, 16 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ (𝑓:{𝐵}⟶𝐴 → {𝑦 ∣ 𝐵𝑓𝑦} = ran 𝑓) |
18 | 17 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑓:{𝐵}⟶𝐴 → ({𝑦 ∣ 𝐵𝑓𝑦} = {𝑦} ↔ ran 𝑓 = {𝑦})) |
19 | 18 | exbidv 1837 |
. . . . . . . 8
⊢ (𝑓:{𝐵}⟶𝐴 → (∃𝑦{𝑦 ∣ 𝐵𝑓𝑦} = {𝑦} ↔ ∃𝑦ran 𝑓 = {𝑦})) |
20 | 9, 19 | syl5bb 271 |
. . . . . . 7
⊢ (𝑓:{𝐵}⟶𝐴 → (∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦ran 𝑓 = {𝑦})) |
21 | 8, 20 | mpbid 221 |
. . . . . 6
⊢ (𝑓:{𝐵}⟶𝐴 → ∃𝑦ran 𝑓 = {𝑦}) |
22 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
23 | 22 | snid 4155 |
. . . . . . . . . 10
⊢ 𝑦 ∈ {𝑦} |
24 | | eleq2 2677 |
. . . . . . . . . 10
⊢ (ran
𝑓 = {𝑦} → (𝑦 ∈ ran 𝑓 ↔ 𝑦 ∈ {𝑦})) |
25 | 23, 24 | mpbiri 247 |
. . . . . . . . 9
⊢ (ran
𝑓 = {𝑦} → 𝑦 ∈ ran 𝑓) |
26 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝑓:{𝐵}⟶𝐴 → ran 𝑓 ⊆ 𝐴) |
27 | 26 | sseld 3567 |
. . . . . . . . 9
⊢ (𝑓:{𝐵}⟶𝐴 → (𝑦 ∈ ran 𝑓 → 𝑦 ∈ 𝐴)) |
28 | 25, 27 | syl5 33 |
. . . . . . . 8
⊢ (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑦 ∈ 𝐴)) |
29 | | dffn4 6034 |
. . . . . . . . . . . 12
⊢ (𝑓 Fn {𝐵} ↔ 𝑓:{𝐵}–onto→ran 𝑓) |
30 | 4, 29 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝑓:{𝐵}⟶𝐴 → 𝑓:{𝐵}–onto→ran 𝑓) |
31 | | fof 6028 |
. . . . . . . . . . 11
⊢ (𝑓:{𝐵}–onto→ran 𝑓 → 𝑓:{𝐵}⟶ran 𝑓) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢ (𝑓:{𝐵}⟶𝐴 → 𝑓:{𝐵}⟶ran 𝑓) |
33 | | feq3 5941 |
. . . . . . . . . 10
⊢ (ran
𝑓 = {𝑦} → (𝑓:{𝐵}⟶ran 𝑓 ↔ 𝑓:{𝐵}⟶{𝑦})) |
34 | 32, 33 | syl5ibcom 234 |
. . . . . . . . 9
⊢ (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑓:{𝐵}⟶{𝑦})) |
35 | 5, 22 | fsn 6308 |
. . . . . . . . 9
⊢ (𝑓:{𝐵}⟶{𝑦} ↔ 𝑓 = {〈𝐵, 𝑦〉}) |
36 | 34, 35 | syl6ib 240 |
. . . . . . . 8
⊢ (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑓 = {〈𝐵, 𝑦〉})) |
37 | 28, 36 | jcad 554 |
. . . . . . 7
⊢ (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → (𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉}))) |
38 | 37 | eximdv 1833 |
. . . . . 6
⊢ (𝑓:{𝐵}⟶𝐴 → (∃𝑦ran 𝑓 = {𝑦} → ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉}))) |
39 | 21, 38 | mpd 15 |
. . . . 5
⊢ (𝑓:{𝐵}⟶𝐴 → ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉})) |
40 | | df-rex 2902 |
. . . . 5
⊢
(∃𝑦 ∈
𝐴 𝑓 = {〈𝐵, 𝑦〉} ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉})) |
41 | 39, 40 | sylibr 223 |
. . . 4
⊢ (𝑓:{𝐵}⟶𝐴 → ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}) |
42 | 5, 22 | f1osn 6088 |
. . . . . . . . 9
⊢
{〈𝐵, 𝑦〉}:{𝐵}–1-1-onto→{𝑦} |
43 | | f1oeq1 6040 |
. . . . . . . . 9
⊢ (𝑓 = {〈𝐵, 𝑦〉} → (𝑓:{𝐵}–1-1-onto→{𝑦} ↔ {〈𝐵, 𝑦〉}:{𝐵}–1-1-onto→{𝑦})) |
44 | 42, 43 | mpbiri 247 |
. . . . . . . 8
⊢ (𝑓 = {〈𝐵, 𝑦〉} → 𝑓:{𝐵}–1-1-onto→{𝑦}) |
45 | | f1of 6050 |
. . . . . . . 8
⊢ (𝑓:{𝐵}–1-1-onto→{𝑦} → 𝑓:{𝐵}⟶{𝑦}) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ (𝑓 = {〈𝐵, 𝑦〉} → 𝑓:{𝐵}⟶{𝑦}) |
47 | | snssi 4280 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → {𝑦} ⊆ 𝐴) |
48 | | fss 5969 |
. . . . . . 7
⊢ ((𝑓:{𝐵}⟶{𝑦} ∧ {𝑦} ⊆ 𝐴) → 𝑓:{𝐵}⟶𝐴) |
49 | 46, 47, 48 | syl2an 493 |
. . . . . 6
⊢ ((𝑓 = {〈𝐵, 𝑦〉} ∧ 𝑦 ∈ 𝐴) → 𝑓:{𝐵}⟶𝐴) |
50 | 49 | expcom 450 |
. . . . 5
⊢ (𝑦 ∈ 𝐴 → (𝑓 = {〈𝐵, 𝑦〉} → 𝑓:{𝐵}⟶𝐴)) |
51 | 50 | rexlimiv 3009 |
. . . 4
⊢
(∃𝑦 ∈
𝐴 𝑓 = {〈𝐵, 𝑦〉} → 𝑓:{𝐵}⟶𝐴) |
52 | 41, 51 | impbii 198 |
. . 3
⊢ (𝑓:{𝐵}⟶𝐴 ↔ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}) |
53 | 3, 52 | bitri 263 |
. 2
⊢ (𝑓 ∈ (𝐴 ↑𝑚 {𝐵}) ↔ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}) |
54 | 53 | abbi2i 2725 |
1
⊢ (𝐴 ↑𝑚
{𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}} |