Metamath Proof Explorer


Theorem ssmapsn

Description: A subset C of a set exponentiation to a singleton, is its projection D exponentiated to the singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ssmapsn.f 𝑓 𝐷
ssmapsn.a ( 𝜑𝐴𝑉 )
ssmapsn.c ( 𝜑𝐶 ⊆ ( 𝐵m { 𝐴 } ) )
ssmapsn.d 𝐷 = 𝑓𝐶 ran 𝑓
Assertion ssmapsn ( 𝜑𝐶 = ( 𝐷m { 𝐴 } ) )

Proof

Step Hyp Ref Expression
1 ssmapsn.f 𝑓 𝐷
2 ssmapsn.a ( 𝜑𝐴𝑉 )
3 ssmapsn.c ( 𝜑𝐶 ⊆ ( 𝐵m { 𝐴 } ) )
4 ssmapsn.d 𝐷 = 𝑓𝐶 ran 𝑓
5 3 sselda ( ( 𝜑𝑓𝐶 ) → 𝑓 ∈ ( 𝐵m { 𝐴 } ) )
6 elmapi ( 𝑓 ∈ ( 𝐵m { 𝐴 } ) → 𝑓 : { 𝐴 } ⟶ 𝐵 )
7 5 6 syl ( ( 𝜑𝑓𝐶 ) → 𝑓 : { 𝐴 } ⟶ 𝐵 )
8 7 ffnd ( ( 𝜑𝑓𝐶 ) → 𝑓 Fn { 𝐴 } )
9 4 a1i ( 𝜑𝐷 = 𝑓𝐶 ran 𝑓 )
10 ovexd ( 𝜑 → ( 𝐵m { 𝐴 } ) ∈ V )
11 10 3 ssexd ( 𝜑𝐶 ∈ V )
12 rnexg ( 𝑓𝐶 → ran 𝑓 ∈ V )
13 12 rgen 𝑓𝐶 ran 𝑓 ∈ V
14 iunexg ( ( 𝐶 ∈ V ∧ ∀ 𝑓𝐶 ran 𝑓 ∈ V ) → 𝑓𝐶 ran 𝑓 ∈ V )
15 11 13 14 sylancl ( 𝜑 𝑓𝐶 ran 𝑓 ∈ V )
16 9 15 eqeltrd ( 𝜑𝐷 ∈ V )
17 16 adantr ( ( 𝜑𝑓𝐶 ) → 𝐷 ∈ V )
18 ssiun2 ( 𝑓𝐶 → ran 𝑓 𝑓𝐶 ran 𝑓 )
19 18 adantl ( ( 𝜑𝑓𝐶 ) → ran 𝑓 𝑓𝐶 ran 𝑓 )
20 snidg ( 𝐴𝑉𝐴 ∈ { 𝐴 } )
21 2 20 syl ( 𝜑𝐴 ∈ { 𝐴 } )
22 21 adantr ( ( 𝜑𝑓𝐶 ) → 𝐴 ∈ { 𝐴 } )
23 8 22 fnfvelrnd ( ( 𝜑𝑓𝐶 ) → ( 𝑓𝐴 ) ∈ ran 𝑓 )
24 19 23 sseldd ( ( 𝜑𝑓𝐶 ) → ( 𝑓𝐴 ) ∈ 𝑓𝐶 ran 𝑓 )
25 24 4 eleqtrrdi ( ( 𝜑𝑓𝐶 ) → ( 𝑓𝐴 ) ∈ 𝐷 )
26 8 17 25 elmapsnd ( ( 𝜑𝑓𝐶 ) → 𝑓 ∈ ( 𝐷m { 𝐴 } ) )
27 16 adantr ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) → 𝐷 ∈ V )
28 snex { 𝐴 } ∈ V
29 28 a1i ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) → { 𝐴 } ∈ V )
30 simpr ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) → 𝑓 ∈ ( 𝐷m { 𝐴 } ) )
31 21 adantr ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) → 𝐴 ∈ { 𝐴 } )
32 27 29 30 31 fvmap ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) → ( 𝑓𝐴 ) ∈ 𝐷 )
33 rneq ( 𝑓 = 𝑔 → ran 𝑓 = ran 𝑔 )
34 33 cbviunv 𝑓𝐶 ran 𝑓 = 𝑔𝐶 ran 𝑔
35 4 34 eqtri 𝐷 = 𝑔𝐶 ran 𝑔
36 32 35 eleqtrdi ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) → ( 𝑓𝐴 ) ∈ 𝑔𝐶 ran 𝑔 )
37 eliun ( ( 𝑓𝐴 ) ∈ 𝑔𝐶 ran 𝑔 ↔ ∃ 𝑔𝐶 ( 𝑓𝐴 ) ∈ ran 𝑔 )
38 36 37 sylib ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) → ∃ 𝑔𝐶 ( 𝑓𝐴 ) ∈ ran 𝑔 )
39 simp3 ( ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) ∧ 𝑔𝐶 ∧ ( 𝑓𝐴 ) ∈ ran 𝑔 ) → ( 𝑓𝐴 ) ∈ ran 𝑔 )
40 simp1l ( ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) ∧ 𝑔𝐶 ∧ ( 𝑓𝐴 ) ∈ ran 𝑔 ) → 𝜑 )
41 40 2 syl ( ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) ∧ 𝑔𝐶 ∧ ( 𝑓𝐴 ) ∈ ran 𝑔 ) → 𝐴𝑉 )
42 eqid { 𝐴 } = { 𝐴 }
43 simp1r ( ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) ∧ 𝑔𝐶 ∧ ( 𝑓𝐴 ) ∈ ran 𝑔 ) → 𝑓 ∈ ( 𝐷m { 𝐴 } ) )
44 elmapfn ( 𝑓 ∈ ( 𝐷m { 𝐴 } ) → 𝑓 Fn { 𝐴 } )
45 43 44 syl ( ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) ∧ 𝑔𝐶 ∧ ( 𝑓𝐴 ) ∈ ran 𝑔 ) → 𝑓 Fn { 𝐴 } )
46 3 sselda ( ( 𝜑𝑔𝐶 ) → 𝑔 ∈ ( 𝐵m { 𝐴 } ) )
47 elmapfn ( 𝑔 ∈ ( 𝐵m { 𝐴 } ) → 𝑔 Fn { 𝐴 } )
48 46 47 syl ( ( 𝜑𝑔𝐶 ) → 𝑔 Fn { 𝐴 } )
49 48 3adant3 ( ( 𝜑𝑔𝐶 ∧ ( 𝑓𝐴 ) ∈ ran 𝑔 ) → 𝑔 Fn { 𝐴 } )
50 49 3adant1r ( ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) ∧ 𝑔𝐶 ∧ ( 𝑓𝐴 ) ∈ ran 𝑔 ) → 𝑔 Fn { 𝐴 } )
51 41 42 45 50 fsneqrn ( ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) ∧ 𝑔𝐶 ∧ ( 𝑓𝐴 ) ∈ ran 𝑔 ) → ( 𝑓 = 𝑔 ↔ ( 𝑓𝐴 ) ∈ ran 𝑔 ) )
52 39 51 mpbird ( ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) ∧ 𝑔𝐶 ∧ ( 𝑓𝐴 ) ∈ ran 𝑔 ) → 𝑓 = 𝑔 )
53 simp2 ( ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) ∧ 𝑔𝐶 ∧ ( 𝑓𝐴 ) ∈ ran 𝑔 ) → 𝑔𝐶 )
54 52 53 eqeltrd ( ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) ∧ 𝑔𝐶 ∧ ( 𝑓𝐴 ) ∈ ran 𝑔 ) → 𝑓𝐶 )
55 54 rexlimdv3a ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) → ( ∃ 𝑔𝐶 ( 𝑓𝐴 ) ∈ ran 𝑔𝑓𝐶 ) )
56 38 55 mpd ( ( 𝜑𝑓 ∈ ( 𝐷m { 𝐴 } ) ) → 𝑓𝐶 )
57 26 56 impbida ( 𝜑 → ( 𝑓𝐶𝑓 ∈ ( 𝐷m { 𝐴 } ) ) )
58 57 alrimiv ( 𝜑 → ∀ 𝑓 ( 𝑓𝐶𝑓 ∈ ( 𝐷m { 𝐴 } ) ) )
59 nfcv 𝑓 𝐶
60 nfcv 𝑓m
61 nfcv 𝑓 { 𝐴 }
62 1 60 61 nfov 𝑓 ( 𝐷m { 𝐴 } )
63 59 62 cleqf ( 𝐶 = ( 𝐷m { 𝐴 } ) ↔ ∀ 𝑓 ( 𝑓𝐶𝑓 ∈ ( 𝐷m { 𝐴 } ) ) )
64 58 63 sylibr ( 𝜑𝐶 = ( 𝐷m { 𝐴 } ) )