Proof of Theorem mapsnd
Step | Hyp | Ref
| Expression |
1 | | mapsnd.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | mapsnd.2 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
3 | | snex 4835 |
. . . . . 6
⊢ {𝐵} ∈ V |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝐵 ∈ 𝑊 → {𝐵} ∈ V) |
5 | 2, 4 | syl 17 |
. . . 4
⊢ (𝜑 → {𝐵} ∈ V) |
6 | | elmapg 7757 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ {𝐵} ∈ V) → (𝑓 ∈ (𝐴 ↑𝑚 {𝐵}) ↔ 𝑓:{𝐵}⟶𝐴)) |
7 | 1, 5, 6 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑓 ∈ (𝐴 ↑𝑚 {𝐵}) ↔ 𝑓:{𝐵}⟶𝐴)) |
8 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝑓:{𝐵}⟶𝐴 → 𝑓 Fn {𝐵}) |
9 | 8 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑓:{𝐵}⟶𝐴 → 𝑓 Fn {𝐵})) |
10 | 9 | imp 444 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → 𝑓 Fn {𝐵}) |
11 | | snidg 4153 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐵}) |
12 | 2, 11 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ {𝐵}) |
13 | 12 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → 𝐵 ∈ {𝐵}) |
14 | | fneu 5909 |
. . . . . . . . 9
⊢ ((𝑓 Fn {𝐵} ∧ 𝐵 ∈ {𝐵}) → ∃!𝑦 𝐵𝑓𝑦) |
15 | 10, 13, 14 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → ∃!𝑦 𝐵𝑓𝑦) |
16 | | euabsn 4205 |
. . . . . . . . . 10
⊢
(∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦{𝑦 ∣ 𝐵𝑓𝑦} = {𝑦}) |
17 | | frel 5963 |
. . . . . . . . . . . . . 14
⊢ (𝑓:{𝐵}⟶𝐴 → Rel 𝑓) |
18 | | relimasn 5407 |
. . . . . . . . . . . . . 14
⊢ (Rel
𝑓 → (𝑓 “ {𝐵}) = {𝑦 ∣ 𝐵𝑓𝑦}) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑓:{𝐵}⟶𝐴 → (𝑓 “ {𝐵}) = {𝑦 ∣ 𝐵𝑓𝑦}) |
20 | | imadmrn 5395 |
. . . . . . . . . . . . . 14
⊢ (𝑓 “ dom 𝑓) = ran 𝑓 |
21 | | fdm 5964 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:{𝐵}⟶𝐴 → dom 𝑓 = {𝐵}) |
22 | 21 | imaeq2d 5385 |
. . . . . . . . . . . . . 14
⊢ (𝑓:{𝐵}⟶𝐴 → (𝑓 “ dom 𝑓) = (𝑓 “ {𝐵})) |
23 | 20, 22 | syl5reqr 2659 |
. . . . . . . . . . . . 13
⊢ (𝑓:{𝐵}⟶𝐴 → (𝑓 “ {𝐵}) = ran 𝑓) |
24 | 19, 23 | eqtr3d 2646 |
. . . . . . . . . . . 12
⊢ (𝑓:{𝐵}⟶𝐴 → {𝑦 ∣ 𝐵𝑓𝑦} = ran 𝑓) |
25 | 24 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑓:{𝐵}⟶𝐴 → ({𝑦 ∣ 𝐵𝑓𝑦} = {𝑦} ↔ ran 𝑓 = {𝑦})) |
26 | 25 | exbidv 1837 |
. . . . . . . . . 10
⊢ (𝑓:{𝐵}⟶𝐴 → (∃𝑦{𝑦 ∣ 𝐵𝑓𝑦} = {𝑦} ↔ ∃𝑦ran 𝑓 = {𝑦})) |
27 | 16, 26 | syl5bb 271 |
. . . . . . . . 9
⊢ (𝑓:{𝐵}⟶𝐴 → (∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦ran 𝑓 = {𝑦})) |
28 | 27 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → (∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦ran 𝑓 = {𝑦})) |
29 | 15, 28 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → ∃𝑦ran 𝑓 = {𝑦}) |
30 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
31 | 30 | snid 4155 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ {𝑦} |
32 | | eleq2 2677 |
. . . . . . . . . . . . . 14
⊢ (ran
𝑓 = {𝑦} → (𝑦 ∈ ran 𝑓 ↔ 𝑦 ∈ {𝑦})) |
33 | 31, 32 | mpbiri 247 |
. . . . . . . . . . . . 13
⊢ (ran
𝑓 = {𝑦} → 𝑦 ∈ ran 𝑓) |
34 | | frn 5966 |
. . . . . . . . . . . . . 14
⊢ (𝑓:{𝐵}⟶𝐴 → ran 𝑓 ⊆ 𝐴) |
35 | 34 | sseld 3567 |
. . . . . . . . . . . . 13
⊢ (𝑓:{𝐵}⟶𝐴 → (𝑦 ∈ ran 𝑓 → 𝑦 ∈ 𝐴)) |
36 | 33, 35 | syl5 33 |
. . . . . . . . . . . 12
⊢ (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑦 ∈ 𝐴)) |
37 | 36 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝑓:{𝐵}⟶𝐴 ∧ ran 𝑓 = {𝑦}) → 𝑦 ∈ 𝐴) |
38 | 37 | adantll 746 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) ∧ ran 𝑓 = {𝑦}) → 𝑦 ∈ 𝐴) |
39 | | dffn4 6034 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 Fn {𝐵} ↔ 𝑓:{𝐵}–onto→ran 𝑓) |
40 | 8, 39 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:{𝐵}⟶𝐴 → 𝑓:{𝐵}–onto→ran 𝑓) |
41 | | fof 6028 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:{𝐵}–onto→ran 𝑓 → 𝑓:{𝐵}⟶ran 𝑓) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑓:{𝐵}⟶𝐴 → 𝑓:{𝐵}⟶ran 𝑓) |
43 | | feq3 5941 |
. . . . . . . . . . . . . 14
⊢ (ran
𝑓 = {𝑦} → (𝑓:{𝐵}⟶ran 𝑓 ↔ 𝑓:{𝐵}⟶{𝑦})) |
44 | 42, 43 | syl5ibcom 234 |
. . . . . . . . . . . . 13
⊢ (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑓:{𝐵}⟶{𝑦})) |
45 | 44 | imp 444 |
. . . . . . . . . . . 12
⊢ ((𝑓:{𝐵}⟶𝐴 ∧ ran 𝑓 = {𝑦}) → 𝑓:{𝐵}⟶{𝑦}) |
46 | 45 | adantll 746 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) ∧ ran 𝑓 = {𝑦}) → 𝑓:{𝐵}⟶{𝑦}) |
47 | 2 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) ∧ ran 𝑓 = {𝑦}) → 𝐵 ∈ 𝑊) |
48 | 30 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) ∧ ran 𝑓 = {𝑦}) → 𝑦 ∈ V) |
49 | | fsng 6310 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ 𝑊 ∧ 𝑦 ∈ V) → (𝑓:{𝐵}⟶{𝑦} ↔ 𝑓 = {〈𝐵, 𝑦〉})) |
50 | 47, 48, 49 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) ∧ ran 𝑓 = {𝑦}) → (𝑓:{𝐵}⟶{𝑦} ↔ 𝑓 = {〈𝐵, 𝑦〉})) |
51 | 46, 50 | mpbid 221 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) ∧ ran 𝑓 = {𝑦}) → 𝑓 = {〈𝐵, 𝑦〉}) |
52 | 38, 51 | jca 553 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) ∧ ran 𝑓 = {𝑦}) → (𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉})) |
53 | 52 | ex 449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → (ran 𝑓 = {𝑦} → (𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉}))) |
54 | 53 | eximdv 1833 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → (∃𝑦ran 𝑓 = {𝑦} → ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉}))) |
55 | 29, 54 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉})) |
56 | | df-rex 2902 |
. . . . . 6
⊢
(∃𝑦 ∈
𝐴 𝑓 = {〈𝐵, 𝑦〉} ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉})) |
57 | 55, 56 | sylibr 223 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}) |
58 | 57 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑓:{𝐵}⟶𝐴 → ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉})) |
59 | 30 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑦 ∈ V) |
60 | | f1osng 6089 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ 𝑊 ∧ 𝑦 ∈ V) → {〈𝐵, 𝑦〉}:{𝐵}–1-1-onto→{𝑦}) |
61 | 2, 59, 60 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → {〈𝐵, 𝑦〉}:{𝐵}–1-1-onto→{𝑦}) |
62 | 61 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 = {〈𝐵, 𝑦〉}) → {〈𝐵, 𝑦〉}:{𝐵}–1-1-onto→{𝑦}) |
63 | | f1oeq1 6040 |
. . . . . . . . . . . 12
⊢ (𝑓 = {〈𝐵, 𝑦〉} → (𝑓:{𝐵}–1-1-onto→{𝑦} ↔ {〈𝐵, 𝑦〉}:{𝐵}–1-1-onto→{𝑦})) |
64 | 63 | bicomd 212 |
. . . . . . . . . . 11
⊢ (𝑓 = {〈𝐵, 𝑦〉} → ({〈𝐵, 𝑦〉}:{𝐵}–1-1-onto→{𝑦} ↔ 𝑓:{𝐵}–1-1-onto→{𝑦})) |
65 | 64 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 = {〈𝐵, 𝑦〉}) → ({〈𝐵, 𝑦〉}:{𝐵}–1-1-onto→{𝑦} ↔ 𝑓:{𝐵}–1-1-onto→{𝑦})) |
66 | 62, 65 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 = {〈𝐵, 𝑦〉}) → 𝑓:{𝐵}–1-1-onto→{𝑦}) |
67 | | f1of 6050 |
. . . . . . . . 9
⊢ (𝑓:{𝐵}–1-1-onto→{𝑦} → 𝑓:{𝐵}⟶{𝑦}) |
68 | 66, 67 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 = {〈𝐵, 𝑦〉}) → 𝑓:{𝐵}⟶{𝑦}) |
69 | 68 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉}) → 𝑓:{𝐵}⟶{𝑦}) |
70 | | snssi 4280 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → {𝑦} ⊆ 𝐴) |
71 | 70 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉}) → {𝑦} ⊆ 𝐴) |
72 | | fss 5969 |
. . . . . . 7
⊢ ((𝑓:{𝐵}⟶{𝑦} ∧ {𝑦} ⊆ 𝐴) → 𝑓:{𝐵}⟶𝐴) |
73 | 69, 71, 72 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑓 = {〈𝐵, 𝑦〉}) → 𝑓:{𝐵}⟶𝐴) |
74 | 73 | 3exp 1256 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐴 → (𝑓 = {〈𝐵, 𝑦〉} → 𝑓:{𝐵}⟶𝐴))) |
75 | 74 | rexlimdv 3012 |
. . . 4
⊢ (𝜑 → (∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉} → 𝑓:{𝐵}⟶𝐴)) |
76 | 58, 75 | impbid 201 |
. . 3
⊢ (𝜑 → (𝑓:{𝐵}⟶𝐴 ↔ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉})) |
77 | 7, 76 | bitrd 267 |
. 2
⊢ (𝜑 → (𝑓 ∈ (𝐴 ↑𝑚 {𝐵}) ↔ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉})) |
78 | 77 | abbi2dv 2729 |
1
⊢ (𝜑 → (𝐴 ↑𝑚 {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}}) |