Metamath Proof Explorer

Theorem ralxpmap

Description: Quantification over functions in terms of quantification over values and punctured functions. (Contributed by Stefan O'Rear, 27-Feb-2015) (Revised by Stefan O'Rear, 5-May-2015)

Ref Expression
Hypothesis ralxpmap.j 
|- ( f = ( g u. { <. J , y >. } ) -> ( ph <-> ps ) )
Assertion ralxpmap 
|- ( J e. T -> ( A. f e. ( S ^m T ) ph <-> A. y e. S A. g e. ( S ^m ( T \ { J } ) ) ps ) )

Proof

Step Hyp Ref Expression
1 ralxpmap.j 
 |-  ( f = ( g u. { <. J , y >. } ) -> ( ph <-> ps ) )
2 vex 
 |-  g e. _V
3 snex 
 |-  { <. J , y >. } e. _V
4 2 3 unex 
 |-  ( g u. { <. J , y >. } ) e. _V
5 simpr 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> f e. ( S ^m T ) )
6 elmapex 
 |-  ( f e. ( S ^m T ) -> ( S e. _V /\ T e. _V ) )
7 6 adantl 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> ( S e. _V /\ T e. _V ) )
8 elmapg 
 |-  ( ( S e. _V /\ T e. _V ) -> ( f e. ( S ^m T ) <-> f : T --> S ) )
9 7 8 syl 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> ( f e. ( S ^m T ) <-> f : T --> S ) )
10 5 9 mpbid 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> f : T --> S )
11 simpl 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> J e. T )
12 10 11 ffvelcdmd 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> ( f ` J ) e. S )
13 difss 
 |-  ( T \ { J } ) C_ T
14 fssres 
 |-  ( ( f : T --> S /\ ( T \ { J } ) C_ T ) -> ( f |` ( T \ { J } ) ) : ( T \ { J } ) --> S )
15 10 13 14 sylancl 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> ( f |` ( T \ { J } ) ) : ( T \ { J } ) --> S )
16 6 simpld 
 |-  ( f e. ( S ^m T ) -> S e. _V )
17 16 adantl 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> S e. _V )
18 7 simprd 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> T e. _V )
19 18 difexd 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> ( T \ { J } ) e. _V )
20 17 19 elmapd 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> ( ( f |` ( T \ { J } ) ) e. ( S ^m ( T \ { J } ) ) <-> ( f |` ( T \ { J } ) ) : ( T \ { J } ) --> S ) )
21 15 20 mpbird 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> ( f |` ( T \ { J } ) ) e. ( S ^m ( T \ { J } ) ) )
22 10 ffnd 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> f Fn T )
23 fnsnsplit 
 |-  ( ( f Fn T /\ J e. T ) -> f = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) )
24 22 11 23 syl2anc 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> f = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) )
25 opeq2 
 |-  ( y = ( f ` J ) -> <. J , y >. = <. J , ( f ` J ) >. )
26 25 sneqd 
 |-  ( y = ( f ` J ) -> { <. J , y >. } = { <. J , ( f ` J ) >. } )
27 26 uneq2d 
 |-  ( y = ( f ` J ) -> ( g u. { <. J , y >. } ) = ( g u. { <. J , ( f ` J ) >. } ) )
28 27 eqeq2d 
 |-  ( y = ( f ` J ) -> ( f = ( g u. { <. J , y >. } ) <-> f = ( g u. { <. J , ( f ` J ) >. } ) ) )
29 uneq1 
 |-  ( g = ( f |` ( T \ { J } ) ) -> ( g u. { <. J , ( f ` J ) >. } ) = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) )
30 29 eqeq2d 
 |-  ( g = ( f |` ( T \ { J } ) ) -> ( f = ( g u. { <. J , ( f ` J ) >. } ) <-> f = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) ) )
31 28 30 rspc2ev 
 |-  ( ( ( f ` J ) e. S /\ ( f |` ( T \ { J } ) ) e. ( S ^m ( T \ { J } ) ) /\ f = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) ) -> E. y e. S E. g e. ( S ^m ( T \ { J } ) ) f = ( g u. { <. J , y >. } ) )
32 12 21 24 31 syl3anc 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> E. y e. S E. g e. ( S ^m ( T \ { J } ) ) f = ( g u. { <. J , y >. } ) )
33 32 ex 
 |-  ( J e. T -> ( f e. ( S ^m T ) -> E. y e. S E. g e. ( S ^m ( T \ { J } ) ) f = ( g u. { <. J , y >. } ) ) )
34 elmapi 
 |-  ( g e. ( S ^m ( T \ { J } ) ) -> g : ( T \ { J } ) --> S )
35 34 ad2antll 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> g : ( T \ { J } ) --> S )
36 f1osng 
 |-  ( ( J e. T /\ y e. _V ) -> { <. J , y >. } : { J } -1-1-onto-> { y } )
37 f1of 
 |-  ( { <. J , y >. } : { J } -1-1-onto-> { y } -> { <. J , y >. } : { J } --> { y } )
38 36 37 syl 
 |-  ( ( J e. T /\ y e. _V ) -> { <. J , y >. } : { J } --> { y } )
39 38 elvd 
 |-  ( J e. T -> { <. J , y >. } : { J } --> { y } )
40 39 adantr 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> { <. J , y >. } : { J } --> { y } )
41 disjdifr 
 |-  ( ( T \ { J } ) i^i { J } ) = (/)
42 41 a1i 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( T \ { J } ) i^i { J } ) = (/) )
43 fun 
 |-  ( ( ( g : ( T \ { J } ) --> S /\ { <. J , y >. } : { J } --> { y } ) /\ ( ( T \ { J } ) i^i { J } ) = (/) ) -> ( g u. { <. J , y >. } ) : ( ( T \ { J } ) u. { J } ) --> ( S u. { y } ) )
44 35 40 42 43 syl21anc 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) : ( ( T \ { J } ) u. { J } ) --> ( S u. { y } ) )
45 simpl 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> J e. T )
46 45 snssd 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> { J } C_ T )
47 undifr 
 |-  ( { J } C_ T <-> ( ( T \ { J } ) u. { J } ) = T )
48 46 47 sylib 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( T \ { J } ) u. { J } ) = T )
49 48 feq2d 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( g u. { <. J , y >. } ) : ( ( T \ { J } ) u. { J } ) --> ( S u. { y } ) <-> ( g u. { <. J , y >. } ) : T --> ( S u. { y } ) ) )
50 44 49 mpbid 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) : T --> ( S u. { y } ) )
51 ssidd 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> S C_ S )
52 snssi 
 |-  ( y e. S -> { y } C_ S )
53 52 ad2antrl 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> { y } C_ S )
54 51 53 unssd 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( S u. { y } ) C_ S )
55 50 54 fssd 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) : T --> S )
56 elmapex 
 |-  ( g e. ( S ^m ( T \ { J } ) ) -> ( S e. _V /\ ( T \ { J } ) e. _V ) )
57 56 ad2antll 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( S e. _V /\ ( T \ { J } ) e. _V ) )
58 57 simpld 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> S e. _V )
59 ssun1 
 |-  T C_ ( T u. { J } )
60 undif1 
 |-  ( ( T \ { J } ) u. { J } ) = ( T u. { J } )
61 57 simprd 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( T \ { J } ) e. _V )
62 snex 
 |-  { J } e. _V
63 unexg 
 |-  ( ( ( T \ { J } ) e. _V /\ { J } e. _V ) -> ( ( T \ { J } ) u. { J } ) e. _V )
64 61 62 63 sylancl 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( T \ { J } ) u. { J } ) e. _V )
65 60 64 eqeltrrid 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( T u. { J } ) e. _V )
66 ssexg 
 |-  ( ( T C_ ( T u. { J } ) /\ ( T u. { J } ) e. _V ) -> T e. _V )
67 59 65 66 sylancr 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> T e. _V )
68 58 67 elmapd 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( g u. { <. J , y >. } ) e. ( S ^m T ) <-> ( g u. { <. J , y >. } ) : T --> S ) )
69 55 68 mpbird 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) e. ( S ^m T ) )
70 eleq1 
 |-  ( f = ( g u. { <. J , y >. } ) -> ( f e. ( S ^m T ) <-> ( g u. { <. J , y >. } ) e. ( S ^m T ) ) )
71 69 70 syl5ibrcom 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( f = ( g u. { <. J , y >. } ) -> f e. ( S ^m T ) ) )
72 71 rexlimdvva 
 |-  ( J e. T -> ( E. y e. S E. g e. ( S ^m ( T \ { J } ) ) f = ( g u. { <. J , y >. } ) -> f e. ( S ^m T ) ) )
73 33 72 impbid 
 |-  ( J e. T -> ( f e. ( S ^m T ) <-> E. y e. S E. g e. ( S ^m ( T \ { J } ) ) f = ( g u. { <. J , y >. } ) ) )
74 1 adantl 
 |-  ( ( J e. T /\ f = ( g u. { <. J , y >. } ) ) -> ( ph <-> ps ) )
75 4 73 74 ralxpxfr2d 
 |-  ( J e. T -> ( A. f e. ( S ^m T ) ph <-> A. y e. S A. g e. ( S ^m ( T \ { J } ) ) ps ) )