Metamath Proof Explorer

Theorem unirnmapsn

Description: Equality theorem for a subset of a set exponentiation, where the exponent is a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses unirnmapsn.A 
|- ( ph -> A e. V )
unirnmapsn.b 
|- ( ph -> B e. W )
unirnmapsn.C 
|- C = { A }
unirnmapsn.x 
|- ( ph -> X C_ ( B ^m C ) )
Assertion unirnmapsn 
|- ( ph -> X = ( ran U. X ^m C ) )

Proof

Step Hyp Ref Expression
1 unirnmapsn.A 
 |-  ( ph -> A e. V )
2 unirnmapsn.b 
 |-  ( ph -> B e. W )
3 unirnmapsn.C 
 |-  C = { A }
4 unirnmapsn.x 
 |-  ( ph -> X C_ ( B ^m C ) )
5 snex 
 |-  { A } e. _V
6 3 5 eqeltri 
 |-  C e. _V
7 6 a1i 
 |-  ( ph -> C e. _V )
8 7 4 unirnmap 
 |-  ( ph -> X C_ ( ran U. X ^m C ) )
9 simpl 
 |-  ( ( ph /\ g e. ( ran U. X ^m C ) ) -> ph )
10 equid 
 |-  g = g
11 rnuni 
 |-  ran U. X = U_ f e. X ran f
12 11 oveq1i 
 |-  ( ran U. X ^m C ) = ( U_ f e. X ran f ^m C )
13 10 12 eleq12i 
 |-  ( g e. ( ran U. X ^m C ) <-> g e. ( U_ f e. X ran f ^m C ) )
14 13 biimpi 
 |-  ( g e. ( ran U. X ^m C ) -> g e. ( U_ f e. X ran f ^m C ) )
15 14 adantl 
 |-  ( ( ph /\ g e. ( ran U. X ^m C ) ) -> g e. ( U_ f e. X ran f ^m C ) )
16 ovexd 
 |-  ( ph -> ( B ^m C ) e. _V )
17 16 4 ssexd 
 |-  ( ph -> X e. _V )
18 rnexg 
 |-  ( f e. X -> ran f e. _V )
19 18 rgen 
 |-  A. f e. X ran f e. _V
20 19 a1i 
 |-  ( ph -> A. f e. X ran f e. _V )
21 iunexg 
 |-  ( ( X e. _V /\ A. f e. X ran f e. _V ) -> U_ f e. X ran f e. _V )
22 17 20 21 syl2anc 
 |-  ( ph -> U_ f e. X ran f e. _V )
23 22 7 elmapd 
 |-  ( ph -> ( g e. ( U_ f e. X ran f ^m C ) <-> g : C --> U_ f e. X ran f ) )
24 23 biimpa 
 |-  ( ( ph /\ g e. ( U_ f e. X ran f ^m C ) ) -> g : C --> U_ f e. X ran f )
25 snidg 
 |-  ( A e. V -> A e. { A } )
26 1 25 syl 
 |-  ( ph -> A e. { A } )
27 26 3 eleqtrrdi 
 |-  ( ph -> A e. C )
28 27 adantr 
 |-  ( ( ph /\ g e. ( U_ f e. X ran f ^m C ) ) -> A e. C )
29 24 28 ffvelrnd 
 |-  ( ( ph /\ g e. ( U_ f e. X ran f ^m C ) ) -> ( g ` A ) e. U_ f e. X ran f )
30 eliun 
 |-  ( ( g ` A ) e. U_ f e. X ran f <-> E. f e. X ( g ` A ) e. ran f )
31 29 30 sylib 
 |-  ( ( ph /\ g e. ( U_ f e. X ran f ^m C ) ) -> E. f e. X ( g ` A ) e. ran f )
32 9 15 31 syl2anc 
 |-  ( ( ph /\ g e. ( ran U. X ^m C ) ) -> E. f e. X ( g ` A ) e. ran f )
33 elmapfn 
 |-  ( g e. ( ran U. X ^m C ) -> g Fn C )
34 33 adantl 
 |-  ( ( ph /\ g e. ( ran U. X ^m C ) ) -> g Fn C )
35 simp3 
 |-  ( ( ph /\ f e. X /\ ( g ` A ) e. ran f ) -> ( g ` A ) e. ran f )
36 1 3ad2ant1 
 |-  ( ( ph /\ f e. X /\ ( g ` A ) e. ran f ) -> A e. V )
37 3 oveq2i 
 |-  ( B ^m C ) = ( B ^m { A } )
38 4 37 sseqtrdi 
 |-  ( ph -> X C_ ( B ^m { A } ) )
39 38 adantr 
 |-  ( ( ph /\ f e. X ) -> X C_ ( B ^m { A } ) )
40 simpr 
 |-  ( ( ph /\ f e. X ) -> f e. X )
41 39 40 sseldd 
 |-  ( ( ph /\ f e. X ) -> f e. ( B ^m { A } ) )
42 2 adantr 
 |-  ( ( ph /\ f e. X ) -> B e. W )
43 5 a1i 
 |-  ( ( ph /\ f e. X ) -> { A } e. _V )
44 42 43 elmapd 
 |-  ( ( ph /\ f e. X ) -> ( f e. ( B ^m { A } ) <-> f : { A } --> B ) )
45 41 44 mpbid 
 |-  ( ( ph /\ f e. X ) -> f : { A } --> B )
46 45 3adant3 
 |-  ( ( ph /\ f e. X /\ ( g ` A ) e. ran f ) -> f : { A } --> B )
47 36 46 rnsnf 
 |-  ( ( ph /\ f e. X /\ ( g ` A ) e. ran f ) -> ran f = { ( f ` A ) } )
48 35 47 eleqtrd 
 |-  ( ( ph /\ f e. X /\ ( g ` A ) e. ran f ) -> ( g ` A ) e. { ( f ` A ) } )
49 fvex 
 |-  ( g ` A ) e. _V
50 49 elsn 
 |-  ( ( g ` A ) e. { ( f ` A ) } <-> ( g ` A ) = ( f ` A ) )
51 48 50 sylib 
 |-  ( ( ph /\ f e. X /\ ( g ` A ) e. ran f ) -> ( g ` A ) = ( f ` A ) )
52 51 3adant1r 
 |-  ( ( ( ph /\ g Fn C ) /\ f e. X /\ ( g ` A ) e. ran f ) -> ( g ` A ) = ( f ` A ) )
53 1 adantr 
 |-  ( ( ph /\ g Fn C ) -> A e. V )
54 53 3ad2ant1 
 |-  ( ( ( ph /\ g Fn C ) /\ f e. X /\ ( g ` A ) e. ran f ) -> A e. V )
55 simp1r 
 |-  ( ( ( ph /\ g Fn C ) /\ f e. X /\ ( g ` A ) e. ran f ) -> g Fn C )
56 41 37 eleqtrrdi 
 |-  ( ( ph /\ f e. X ) -> f e. ( B ^m C ) )
57 elmapfn 
 |-  ( f e. ( B ^m C ) -> f Fn C )
58 56 57 syl 
 |-  ( ( ph /\ f e. X ) -> f Fn C )
59 58 adantlr 
 |-  ( ( ( ph /\ g Fn C ) /\ f e. X ) -> f Fn C )
60 59 3adant3 
 |-  ( ( ( ph /\ g Fn C ) /\ f e. X /\ ( g ` A ) e. ran f ) -> f Fn C )
61 54 3 55 60 fsneq 
 |-  ( ( ( ph /\ g Fn C ) /\ f e. X /\ ( g ` A ) e. ran f ) -> ( g = f <-> ( g ` A ) = ( f ` A ) ) )
62 52 61 mpbird 
 |-  ( ( ( ph /\ g Fn C ) /\ f e. X /\ ( g ` A ) e. ran f ) -> g = f )
63 simp2 
 |-  ( ( ( ph /\ g Fn C ) /\ f e. X /\ ( g ` A ) e. ran f ) -> f e. X )
64 62 63 eqeltrd 
 |-  ( ( ( ph /\ g Fn C ) /\ f e. X /\ ( g ` A ) e. ran f ) -> g e. X )
65 64 3exp 
 |-  ( ( ph /\ g Fn C ) -> ( f e. X -> ( ( g ` A ) e. ran f -> g e. X ) ) )
66 9 34 65 syl2anc 
 |-  ( ( ph /\ g e. ( ran U. X ^m C ) ) -> ( f e. X -> ( ( g ` A ) e. ran f -> g e. X ) ) )
67 66 rexlimdv 
 |-  ( ( ph /\ g e. ( ran U. X ^m C ) ) -> ( E. f e. X ( g ` A ) e. ran f -> g e. X ) )
68 32 67 mpd 
 |-  ( ( ph /\ g e. ( ran U. X ^m C ) ) -> g e. X )
69 8 68 eqelssd 
 |-  ( ph -> X = ( ran U. X ^m C ) )