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
|- F/_ f D
ssmapsn.a
|- ( ph -> A e. V )
ssmapsn.c
|- ( ph -> C C_ ( B ^m { A } ) )
ssmapsn.d
|- D = U_ f e. C ran f
Assertion ssmapsn
|- ( ph -> C = ( D ^m { A } ) )

Proof

Step Hyp Ref Expression
1 ssmapsn.f
 |-  F/_ f D
2 ssmapsn.a
 |-  ( ph -> A e. V )
3 ssmapsn.c
 |-  ( ph -> C C_ ( B ^m { A } ) )
4 ssmapsn.d
 |-  D = U_ f e. C ran f
5 3 sselda
 |-  ( ( ph /\ f e. C ) -> f e. ( B ^m { A } ) )
6 elmapi
 |-  ( f e. ( B ^m { A } ) -> f : { A } --> B )
7 5 6 syl
 |-  ( ( ph /\ f e. C ) -> f : { A } --> B )
8 7 ffnd
 |-  ( ( ph /\ f e. C ) -> f Fn { A } )
9 4 a1i
 |-  ( ph -> D = U_ f e. C ran f )
10 ovexd
 |-  ( ph -> ( B ^m { A } ) e. _V )
11 10 3 ssexd
 |-  ( ph -> C e. _V )
12 rnexg
 |-  ( f e. C -> ran f e. _V )
13 12 rgen
 |-  A. f e. C ran f e. _V
14 iunexg
 |-  ( ( C e. _V /\ A. f e. C ran f e. _V ) -> U_ f e. C ran f e. _V )
15 11 13 14 sylancl
 |-  ( ph -> U_ f e. C ran f e. _V )
16 9 15 eqeltrd
 |-  ( ph -> D e. _V )
17 16 adantr
 |-  ( ( ph /\ f e. C ) -> D e. _V )
18 ssiun2
 |-  ( f e. C -> ran f C_ U_ f e. C ran f )
19 18 adantl
 |-  ( ( ph /\ f e. C ) -> ran f C_ U_ f e. C ran f )
20 snidg
 |-  ( A e. V -> A e. { A } )
21 2 20 syl
 |-  ( ph -> A e. { A } )
22 21 adantr
 |-  ( ( ph /\ f e. C ) -> A e. { A } )
23 8 22 fnfvelrnd
 |-  ( ( ph /\ f e. C ) -> ( f ` A ) e. ran f )
24 19 23 sseldd
 |-  ( ( ph /\ f e. C ) -> ( f ` A ) e. U_ f e. C ran f )
25 24 4 eleqtrrdi
 |-  ( ( ph /\ f e. C ) -> ( f ` A ) e. D )
26 8 17 25 elmapsnd
 |-  ( ( ph /\ f e. C ) -> f e. ( D ^m { A } ) )
27 16 adantr
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> D e. _V )
28 snex
 |-  { A } e. _V
29 28 a1i
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> { A } e. _V )
30 simpr
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> f e. ( D ^m { A } ) )
31 21 adantr
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> A e. { A } )
32 27 29 30 31 fvmap
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> ( f ` A ) e. D )
33 rneq
 |-  ( f = g -> ran f = ran g )
34 33 cbviunv
 |-  U_ f e. C ran f = U_ g e. C ran g
35 4 34 eqtri
 |-  D = U_ g e. C ran g
36 32 35 eleqtrdi
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> ( f ` A ) e. U_ g e. C ran g )
37 eliun
 |-  ( ( f ` A ) e. U_ g e. C ran g <-> E. g e. C ( f ` A ) e. ran g )
38 36 37 sylib
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> E. g e. C ( f ` A ) e. ran g )
39 simp3
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> ( f ` A ) e. ran g )
40 simp1l
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> ph )
41 40 2 syl
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> A e. V )
42 eqid
 |-  { A } = { A }
43 simp1r
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> f e. ( D ^m { A } ) )
44 elmapfn
 |-  ( f e. ( D ^m { A } ) -> f Fn { A } )
45 43 44 syl
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> f Fn { A } )
46 3 sselda
 |-  ( ( ph /\ g e. C ) -> g e. ( B ^m { A } ) )
47 elmapfn
 |-  ( g e. ( B ^m { A } ) -> g Fn { A } )
48 46 47 syl
 |-  ( ( ph /\ g e. C ) -> g Fn { A } )
49 48 3adant3
 |-  ( ( ph /\ g e. C /\ ( f ` A ) e. ran g ) -> g Fn { A } )
50 49 3adant1r
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> g Fn { A } )
51 41 42 45 50 fsneqrn
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> ( f = g <-> ( f ` A ) e. ran g ) )
52 39 51 mpbird
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> f = g )
53 simp2
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> g e. C )
54 52 53 eqeltrd
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> f e. C )
55 54 rexlimdv3a
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> ( E. g e. C ( f ` A ) e. ran g -> f e. C ) )
56 38 55 mpd
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> f e. C )
57 26 56 impbida
 |-  ( ph -> ( f e. C <-> f e. ( D ^m { A } ) ) )
58 57 alrimiv
 |-  ( ph -> A. f ( f e. C <-> f e. ( D ^m { A } ) ) )
59 nfcv
 |-  F/_ f C
60 nfcv
 |-  F/_ f ^m
61 nfcv
 |-  F/_ f { A }
62 1 60 61 nfov
 |-  F/_ f ( D ^m { A } )
63 59 62 cleqf
 |-  ( C = ( D ^m { A } ) <-> A. f ( f e. C <-> f e. ( D ^m { A } ) ) )
64 58 63 sylibr
 |-  ( ph -> C = ( D ^m { A } ) )