Proof of Theorem mapsn
Step | Hyp | Ref
| Expression |
1 | | map0.1 |
. . . 4
⊢ 𝐴 ∈ V |
2 | | snex 4908 |
. . . 4
⊢ {𝐵} ∈ V |
3 | 1, 2 | elmap 7886 |
. . 3
⊢ (𝑓 ∈ (𝐴 ↑𝑚 {𝐵}) ↔ 𝑓:{𝐵}⟶𝐴) |
4 | | ffn 6045 |
. . . . . . . 8
⊢ (𝑓:{𝐵}⟶𝐴 → 𝑓 Fn {𝐵}) |
5 | | map0.2 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
6 | 5 | snid 4208 |
. . . . . . . 8
⊢ 𝐵 ∈ {𝐵} |
7 | | fneu 5995 |
. . . . . . . 8
⊢ ((𝑓 Fn {𝐵} ∧ 𝐵 ∈ {𝐵}) → ∃!𝑦 𝐵𝑓𝑦) |
8 | 4, 6, 7 | sylancl 694 |
. . . . . . 7
⊢ (𝑓:{𝐵}⟶𝐴 → ∃!𝑦 𝐵𝑓𝑦) |
9 | | euabsn 4261 |
. . . . . . . 8
⊢
(∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦{𝑦 ∣ 𝐵𝑓𝑦} = {𝑦}) |
10 | | frel 6050 |
. . . . . . . . . . . 12
⊢ (𝑓:{𝐵}⟶𝐴 → Rel 𝑓) |
11 | | relimasn 5488 |
. . . . . . . . . . . 12
⊢ (Rel
𝑓 → (𝑓 “ {𝐵}) = {𝑦 ∣ 𝐵𝑓𝑦}) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑓:{𝐵}⟶𝐴 → (𝑓 “ {𝐵}) = {𝑦 ∣ 𝐵𝑓𝑦}) |
13 | | imadmrn 5476 |
. . . . . . . . . . . 12
⊢ (𝑓 “ dom 𝑓) = ran 𝑓 |
14 | | fdm 6051 |
. . . . . . . . . . . . 13
⊢ (𝑓:{𝐵}⟶𝐴 → dom 𝑓 = {𝐵}) |
15 | 14 | imaeq2d 5466 |
. . . . . . . . . . . 12
⊢ (𝑓:{𝐵}⟶𝐴 → (𝑓 “ dom 𝑓) = (𝑓 “ {𝐵})) |
16 | 13, 15 | syl5reqr 2671 |
. . . . . . . . . . 11
⊢ (𝑓:{𝐵}⟶𝐴 → (𝑓 “ {𝐵}) = ran 𝑓) |
17 | 12, 16 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ (𝑓:{𝐵}⟶𝐴 → {𝑦 ∣ 𝐵𝑓𝑦} = ran 𝑓) |
18 | 17 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑓:{𝐵}⟶𝐴 → ({𝑦 ∣ 𝐵𝑓𝑦} = {𝑦} ↔ ran 𝑓 = {𝑦})) |
19 | 18 | exbidv 1850 |
. . . . . . . 8
⊢ (𝑓:{𝐵}⟶𝐴 → (∃𝑦{𝑦 ∣ 𝐵𝑓𝑦} = {𝑦} ↔ ∃𝑦ran 𝑓 = {𝑦})) |
20 | 9, 19 | syl5bb 272 |
. . . . . . 7
⊢ (𝑓:{𝐵}⟶𝐴 → (∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦ran 𝑓 = {𝑦})) |
21 | 8, 20 | mpbid 222 |
. . . . . 6
⊢ (𝑓:{𝐵}⟶𝐴 → ∃𝑦ran 𝑓 = {𝑦}) |
22 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
23 | 22 | snid 4208 |
. . . . . . . . . 10
⊢ 𝑦 ∈ {𝑦} |
24 | | eleq2 2690 |
. . . . . . . . . 10
⊢ (ran
𝑓 = {𝑦} → (𝑦 ∈ ran 𝑓 ↔ 𝑦 ∈ {𝑦})) |
25 | 23, 24 | mpbiri 248 |
. . . . . . . . 9
⊢ (ran
𝑓 = {𝑦} → 𝑦 ∈ ran 𝑓) |
26 | | frn 6053 |
. . . . . . . . . 10
⊢ (𝑓:{𝐵}⟶𝐴 → ran 𝑓 ⊆ 𝐴) |
27 | 26 | sseld 3602 |
. . . . . . . . 9
⊢ (𝑓:{𝐵}⟶𝐴 → (𝑦 ∈ ran 𝑓 → 𝑦 ∈ 𝐴)) |
28 | 25, 27 | syl5 34 |
. . . . . . . 8
⊢ (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑦 ∈ 𝐴)) |
29 | | dffn4 6121 |
. . . . . . . . . . . 12
⊢ (𝑓 Fn {𝐵} ↔ 𝑓:{𝐵}–onto→ran 𝑓) |
30 | 4, 29 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝑓:{𝐵}⟶𝐴 → 𝑓:{𝐵}–onto→ran 𝑓) |
31 | | fof 6115 |
. . . . . . . . . . 11
⊢ (𝑓:{𝐵}–onto→ran 𝑓 → 𝑓:{𝐵}⟶ran 𝑓) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢ (𝑓:{𝐵}⟶𝐴 → 𝑓:{𝐵}⟶ran 𝑓) |
33 | | feq3 6028 |
. . . . . . . . . 10
⊢ (ran
𝑓 = {𝑦} → (𝑓:{𝐵}⟶ran 𝑓 ↔ 𝑓:{𝐵}⟶{𝑦})) |
34 | 32, 33 | syl5ibcom 235 |
. . . . . . . . 9
⊢ (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑓:{𝐵}⟶{𝑦})) |
35 | 5, 22 | fsn 6402 |
. . . . . . . . 9
⊢ (𝑓:{𝐵}⟶{𝑦} ↔ 𝑓 = {〈𝐵, 𝑦〉}) |
36 | 34, 35 | syl6ib 241 |
. . . . . . . 8
⊢ (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑓 = {〈𝐵, 𝑦〉})) |
37 | 28, 36 | jcad 555 |
. . . . . . 7
⊢ (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → (𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉}))) |
38 | 37 | eximdv 1846 |
. . . . . 6
⊢ (𝑓:{𝐵}⟶𝐴 → (∃𝑦ran 𝑓 = {𝑦} → ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉}))) |
39 | 21, 38 | mpd 15 |
. . . . 5
⊢ (𝑓:{𝐵}⟶𝐴 → ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉})) |
40 | | df-rex 2918 |
. . . . 5
⊢
(∃𝑦 ∈
𝐴 𝑓 = {〈𝐵, 𝑦〉} ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉})) |
41 | 39, 40 | sylibr 224 |
. . . 4
⊢ (𝑓:{𝐵}⟶𝐴 → ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}) |
42 | 5, 22 | f1osn 6176 |
. . . . . . . . 9
⊢
{〈𝐵, 𝑦〉}:{𝐵}–1-1-onto→{𝑦} |
43 | | f1oeq1 6127 |
. . . . . . . . 9
⊢ (𝑓 = {〈𝐵, 𝑦〉} → (𝑓:{𝐵}–1-1-onto→{𝑦} ↔ {〈𝐵, 𝑦〉}:{𝐵}–1-1-onto→{𝑦})) |
44 | 42, 43 | mpbiri 248 |
. . . . . . . 8
⊢ (𝑓 = {〈𝐵, 𝑦〉} → 𝑓:{𝐵}–1-1-onto→{𝑦}) |
45 | | f1of 6137 |
. . . . . . . 8
⊢ (𝑓:{𝐵}–1-1-onto→{𝑦} → 𝑓:{𝐵}⟶{𝑦}) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ (𝑓 = {〈𝐵, 𝑦〉} → 𝑓:{𝐵}⟶{𝑦}) |
47 | | snssi 4339 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → {𝑦} ⊆ 𝐴) |
48 | | fss 6056 |
. . . . . . 7
⊢ ((𝑓:{𝐵}⟶{𝑦} ∧ {𝑦} ⊆ 𝐴) → 𝑓:{𝐵}⟶𝐴) |
49 | 46, 47, 48 | syl2an 494 |
. . . . . 6
⊢ ((𝑓 = {〈𝐵, 𝑦〉} ∧ 𝑦 ∈ 𝐴) → 𝑓:{𝐵}⟶𝐴) |
50 | 49 | expcom 451 |
. . . . 5
⊢ (𝑦 ∈ 𝐴 → (𝑓 = {〈𝐵, 𝑦〉} → 𝑓:{𝐵}⟶𝐴)) |
51 | 50 | rexlimiv 3027 |
. . . 4
⊢
(∃𝑦 ∈
𝐴 𝑓 = {〈𝐵, 𝑦〉} → 𝑓:{𝐵}⟶𝐴) |
52 | 41, 51 | impbii 199 |
. . 3
⊢ (𝑓:{𝐵}⟶𝐴 ↔ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}) |
53 | 3, 52 | bitri 264 |
. 2
⊢ (𝑓 ∈ (𝐴 ↑𝑚 {𝐵}) ↔ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}) |
54 | 53 | abbi2i 2738 |
1
⊢ (𝐴 ↑𝑚
{𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}} |