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

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