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 13 a1i 
 |-  ( ph -> A. f e. C ran f e. _V )
15 11 14 jca 
 |-  ( ph -> ( C e. _V /\ A. f e. C ran f e. _V ) )
16 iunexg 
 |-  ( ( C e. _V /\ A. f e. C ran f e. _V ) -> U_ f e. C ran f e. _V )
17 15 16 syl 
 |-  ( ph -> U_ f e. C ran f e. _V )
18 9 17 eqeltrd 
 |-  ( ph -> D e. _V )
19 18 adantr 
 |-  ( ( ph /\ f e. C ) -> D e. _V )
20 ssiun2 
 |-  ( f e. C -> ran f C_ U_ f e. C ran f )
21 20 adantl 
 |-  ( ( ph /\ f e. C ) -> ran f C_ U_ f e. C ran f )
22 snidg 
 |-  ( A e. V -> A e. { A } )
23 2 22 syl 
 |-  ( ph -> A e. { A } )
24 23 adantr 
 |-  ( ( ph /\ f e. C ) -> A e. { A } )
25 fnfvelrn 
 |-  ( ( f Fn { A } /\ A e. { A } ) -> ( f ` A ) e. ran f )
26 8 24 25 syl2anc 
 |-  ( ( ph /\ f e. C ) -> ( f ` A ) e. ran f )
27 21 26 sseldd 
 |-  ( ( ph /\ f e. C ) -> ( f ` A ) e. U_ f e. C ran f )
28 27 4 eleqtrrdi 
 |-  ( ( ph /\ f e. C ) -> ( f ` A ) e. D )
29 8 19 28 elmapsnd 
 |-  ( ( ph /\ f e. C ) -> f e. ( D ^m { A } ) )
30 29 ex 
 |-  ( ph -> ( f e. C -> f e. ( D ^m { A } ) ) )
31 18 adantr 
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> D e. _V )
32 snex 
 |-  { A } e. _V
33 32 a1i 
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> { A } e. _V )
34 simpr 
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> f e. ( D ^m { A } ) )
35 23 adantr 
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> A e. { A } )
36 31 33 34 35 fvmap 
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> ( f ` A ) e. D )
37 4 idi 
 |-  D = U_ f e. C ran f
38 rneq 
 |-  ( f = g -> ran f = ran g )
39 38 cbviunv 
 |-  U_ f e. C ran f = U_ g e. C ran g
40 37 39 eqtri 
 |-  D = U_ g e. C ran g
41 36 40 eleqtrdi 
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> ( f ` A ) e. U_ g e. C ran g )
42 eliun 
 |-  ( ( f ` A ) e. U_ g e. C ran g <-> E. g e. C ( f ` A ) e. ran g )
43 41 42 sylib 
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> E. g e. C ( f ` A ) e. ran g )
44 simp3 
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> ( f ` A ) e. ran g )
45 simp1l 
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> ph )
46 45 2 syl 
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> A e. V )
47 eqid 
 |-  { A } = { A }
48 simp1r 
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> f e. ( D ^m { A } ) )
49 elmapfn 
 |-  ( f e. ( D ^m { A } ) -> f Fn { A } )
50 48 49 syl 
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> f Fn { A } )
51 3 sselda 
 |-  ( ( ph /\ g e. C ) -> g e. ( B ^m { A } ) )
52 elmapfn 
 |-  ( g e. ( B ^m { A } ) -> g Fn { A } )
53 51 52 syl 
 |-  ( ( ph /\ g e. C ) -> g Fn { A } )
54 53 3adant3 
 |-  ( ( ph /\ g e. C /\ ( f ` A ) e. ran g ) -> g Fn { A } )
55 54 3adant1r 
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> g Fn { A } )
56 46 47 50 55 fsneqrn 
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> ( f = g <-> ( f ` A ) e. ran g ) )
57 44 56 mpbird 
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> f = g )
58 simp2 
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> g e. C )
59 57 58 eqeltrd 
 |-  ( ( ( ph /\ f e. ( D ^m { A } ) ) /\ g e. C /\ ( f ` A ) e. ran g ) -> f e. C )
60 59 3exp 
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> ( g e. C -> ( ( f ` A ) e. ran g -> f e. C ) ) )
61 60 rexlimdv 
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> ( E. g e. C ( f ` A ) e. ran g -> f e. C ) )
62 43 61 mpd 
 |-  ( ( ph /\ f e. ( D ^m { A } ) ) -> f e. C )
63 62 ex 
 |-  ( ph -> ( f e. ( D ^m { A } ) -> f e. C ) )
64 30 63 impbid 
 |-  ( ph -> ( f e. C <-> f e. ( D ^m { A } ) ) )
65 64 alrimiv 
 |-  ( ph -> A. f ( f e. C <-> f e. ( D ^m { A } ) ) )
66 nfcv 
 |-  F/_ f C
67 nfcv 
 |-  F/_ f ^m
68 nfcv 
 |-  F/_ f { A }
69 1 67 68 nfov 
 |-  F/_ f ( D ^m { A } )
70 66 69 cleqf 
 |-  ( C = ( D ^m { A } ) <-> A. f ( f e. C <-> f e. ( D ^m { A } ) ) )
71 65 70 sylibr 
 |-  ( ph -> C = ( D ^m { A } ) )