Step | Hyp | Ref
| Expression |
1 | | ssmapsn.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ⊆ (𝐵 ↑𝑚 {𝐴})) |
2 | 1 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝑓 ∈ (𝐵 ↑𝑚 {𝐴})) |
3 | | elmapi 7765 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝐵 ↑𝑚 {𝐴}) → 𝑓:{𝐴}⟶𝐵) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝑓:{𝐴}⟶𝐵) |
5 | 4 | ffnd 5959 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝑓 Fn {𝐴}) |
6 | | ssmapsn.d |
. . . . . . . . 9
⊢ 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓 |
7 | 6 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓) |
8 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (𝐵 ↑𝑚
{𝐴}) ∈
V |
9 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 ↑𝑚 {𝐴}) ∈ V) |
10 | 9, 1 | ssexd 4733 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ V) |
11 | | rnexg 6990 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ 𝐶 → ran 𝑓 ∈ V) |
12 | 11 | rgen 2906 |
. . . . . . . . . . 11
⊢
∀𝑓 ∈
𝐶 ran 𝑓 ∈ V |
13 | 12 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑓 ∈ 𝐶 ran 𝑓 ∈ V) |
14 | 10, 13 | jca 553 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ∈ V ∧ ∀𝑓 ∈ 𝐶 ran 𝑓 ∈ V)) |
15 | | iunexg 7035 |
. . . . . . . . 9
⊢ ((𝐶 ∈ V ∧ ∀𝑓 ∈ 𝐶 ran 𝑓 ∈ V) → ∪ 𝑓 ∈ 𝐶 ran 𝑓 ∈ V) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑓 ∈ 𝐶 ran 𝑓 ∈ V) |
17 | 7, 16 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ V) |
18 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝐷 ∈ V) |
19 | | ssiun2 4499 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝐶 → ran 𝑓 ⊆ ∪
𝑓 ∈ 𝐶 ran 𝑓) |
20 | 19 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → ran 𝑓 ⊆ ∪
𝑓 ∈ 𝐶 ran 𝑓) |
21 | | ssmapsn.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
22 | | snidg 4153 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
23 | 21, 22 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
24 | 23 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝐴 ∈ {𝐴}) |
25 | | fnfvelrn 6264 |
. . . . . . . . 9
⊢ ((𝑓 Fn {𝐴} ∧ 𝐴 ∈ {𝐴}) → (𝑓‘𝐴) ∈ ran 𝑓) |
26 | 5, 24, 25 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → (𝑓‘𝐴) ∈ ran 𝑓) |
27 | 20, 26 | sseldd 3569 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → (𝑓‘𝐴) ∈ ∪
𝑓 ∈ 𝐶 ran 𝑓) |
28 | 27, 6 | syl6eleqr 2699 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → (𝑓‘𝐴) ∈ 𝐷) |
29 | 5, 18, 28 | elmapsnd 38391 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) |
30 | 29 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑓 ∈ 𝐶 → 𝑓 ∈ (𝐷 ↑𝑚 {𝐴}))) |
31 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) → 𝐷 ∈ V) |
32 | | snex 4835 |
. . . . . . . . . 10
⊢ {𝐴} ∈ V |
33 | 32 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) → {𝐴} ∈ V) |
34 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) → 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) |
35 | 23 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) → 𝐴 ∈ {𝐴}) |
36 | 31, 33, 34, 35 | fvmap 38382 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) → (𝑓‘𝐴) ∈ 𝐷) |
37 | 6 | idi 2 |
. . . . . . . . 9
⊢ 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓 |
38 | | rneq 5272 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → ran 𝑓 = ran 𝑔) |
39 | 38 | cbviunv 4495 |
. . . . . . . . 9
⊢ ∪ 𝑓 ∈ 𝐶 ran 𝑓 = ∪ 𝑔 ∈ 𝐶 ran 𝑔 |
40 | 37, 39 | eqtri 2632 |
. . . . . . . 8
⊢ 𝐷 = ∪ 𝑔 ∈ 𝐶 ran 𝑔 |
41 | 36, 40 | syl6eleq 2698 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) → (𝑓‘𝐴) ∈ ∪
𝑔 ∈ 𝐶 ran 𝑔) |
42 | | eliun 4460 |
. . . . . . 7
⊢ ((𝑓‘𝐴) ∈ ∪
𝑔 ∈ 𝐶 ran 𝑔 ↔ ∃𝑔 ∈ 𝐶 (𝑓‘𝐴) ∈ ran 𝑔) |
43 | 41, 42 | sylib 207 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) → ∃𝑔 ∈ 𝐶 (𝑓‘𝐴) ∈ ran 𝑔) |
44 | | simp3 1056 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → (𝑓‘𝐴) ∈ ran 𝑔) |
45 | | simp1l 1078 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝜑) |
46 | 45, 21 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝐴 ∈ 𝑉) |
47 | | eqid 2610 |
. . . . . . . . . . 11
⊢ {𝐴} = {𝐴} |
48 | | simp1r 1079 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) |
49 | | elmapfn 7766 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (𝐷 ↑𝑚 {𝐴}) → 𝑓 Fn {𝐴}) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝑓 Fn {𝐴}) |
51 | 1 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → 𝑔 ∈ (𝐵 ↑𝑚 {𝐴})) |
52 | | elmapfn 7766 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (𝐵 ↑𝑚 {𝐴}) → 𝑔 Fn {𝐴}) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → 𝑔 Fn {𝐴}) |
54 | 53 | 3adant3 1074 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝑔 Fn {𝐴}) |
55 | 54 | 3adant1r 1311 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝑔 Fn {𝐴}) |
56 | 46, 47, 50, 55 | fsneqrn 38398 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → (𝑓 = 𝑔 ↔ (𝑓‘𝐴) ∈ ran 𝑔)) |
57 | 44, 56 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝑓 = 𝑔) |
58 | | simp2 1055 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝑔 ∈ 𝐶) |
59 | 57, 58 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝑓 ∈ 𝐶) |
60 | 59 | 3exp 1256 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) → (𝑔 ∈ 𝐶 → ((𝑓‘𝐴) ∈ ran 𝑔 → 𝑓 ∈ 𝐶))) |
61 | 60 | rexlimdv 3012 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) → (∃𝑔 ∈ 𝐶 (𝑓‘𝐴) ∈ ran 𝑔 → 𝑓 ∈ 𝐶)) |
62 | 43, 61 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴})) → 𝑓 ∈ 𝐶) |
63 | 62 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑓 ∈ (𝐷 ↑𝑚 {𝐴}) → 𝑓 ∈ 𝐶)) |
64 | 30, 63 | impbid 201 |
. . 3
⊢ (𝜑 → (𝑓 ∈ 𝐶 ↔ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴}))) |
65 | 64 | alrimiv 1842 |
. 2
⊢ (𝜑 → ∀𝑓(𝑓 ∈ 𝐶 ↔ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴}))) |
66 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑓𝐶 |
67 | | ssmapsn.f |
. . . 4
⊢
Ⅎ𝑓𝐷 |
68 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑓
↑𝑚 |
69 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑓{𝐴} |
70 | 67, 68, 69 | nfov 6575 |
. . 3
⊢
Ⅎ𝑓(𝐷 ↑𝑚 {𝐴}) |
71 | 66, 70 | dfcleqf 38281 |
. 2
⊢ (𝐶 = (𝐷 ↑𝑚 {𝐴}) ↔ ∀𝑓(𝑓 ∈ 𝐶 ↔ 𝑓 ∈ (𝐷 ↑𝑚 {𝐴}))) |
72 | 65, 71 | sylibr 223 |
1
⊢ (𝜑 → 𝐶 = (𝐷 ↑𝑚 {𝐴})) |