This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } ) )