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 ffvelrnd 
 |-  ( ( 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 difexg 
 |-  ( T e. _V -> ( T \ { J } ) e. _V )
20 18 19 syl 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> ( T \ { J } ) e. _V )
21 17 20 elmapd 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> ( ( f |` ( T \ { J } ) ) e. ( S ^m ( T \ { J } ) ) <-> ( f |` ( T \ { J } ) ) : ( T \ { J } ) --> S ) )
22 15 21 mpbird 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> ( f |` ( T \ { J } ) ) e. ( S ^m ( T \ { J } ) ) )
23 10 ffnd 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> f Fn T )
24 fnsnsplit 
 |-  ( ( f Fn T /\ J e. T ) -> f = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) )
25 23 11 24 syl2anc 
 |-  ( ( J e. T /\ f e. ( S ^m T ) ) -> f = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) )
26 opeq2 
 |-  ( y = ( f ` J ) -> <. J , y >. = <. J , ( f ` J ) >. )
27 26 sneqd 
 |-  ( y = ( f ` J ) -> { <. J , y >. } = { <. J , ( f ` J ) >. } )
28 27 uneq2d 
 |-  ( y = ( f ` J ) -> ( g u. { <. J , y >. } ) = ( g u. { <. J , ( f ` J ) >. } ) )
29 28 eqeq2d 
 |-  ( y = ( f ` J ) -> ( f = ( g u. { <. J , y >. } ) <-> f = ( g u. { <. J , ( f ` J ) >. } ) ) )
30 uneq1 
 |-  ( g = ( f |` ( T \ { J } ) ) -> ( g u. { <. J , ( f ` J ) >. } ) = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) )
31 30 eqeq2d 
 |-  ( g = ( f |` ( T \ { J } ) ) -> ( f = ( g u. { <. J , ( f ` J ) >. } ) <-> f = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) ) )
32 29 31 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 >. } ) )
33 12 22 25 32 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 >. } ) )
34 33 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 >. } ) ) )
35 elmapi 
 |-  ( g e. ( S ^m ( T \ { J } ) ) -> g : ( T \ { J } ) --> S )
36 35 ad2antll 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> g : ( T \ { J } ) --> S )
37 f1osng 
 |-  ( ( J e. T /\ y e. _V ) -> { <. J , y >. } : { J } -1-1-onto-> { y } )
38 f1of 
 |-  ( { <. J , y >. } : { J } -1-1-onto-> { y } -> { <. J , y >. } : { J } --> { y } )
39 37 38 syl 
 |-  ( ( J e. T /\ y e. _V ) -> { <. J , y >. } : { J } --> { y } )
40 39 elvd 
 |-  ( J e. T -> { <. J , y >. } : { J } --> { y } )
41 40 adantr 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> { <. J , y >. } : { J } --> { y } )
42 incom 
 |-  ( ( T \ { J } ) i^i { J } ) = ( { J } i^i ( T \ { J } ) )
43 disjdif 
 |-  ( { J } i^i ( T \ { J } ) ) = (/)
44 42 43 eqtri 
 |-  ( ( T \ { J } ) i^i { J } ) = (/)
45 44 a1i 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( T \ { J } ) i^i { J } ) = (/) )
46 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 } ) )
47 36 41 45 46 syl21anc 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) : ( ( T \ { J } ) u. { J } ) --> ( S u. { y } ) )
48 uncom 
 |-  ( ( T \ { J } ) u. { J } ) = ( { J } u. ( T \ { J } ) )
49 simpl 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> J e. T )
50 49 snssd 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> { J } C_ T )
51 undif 
 |-  ( { J } C_ T <-> ( { J } u. ( T \ { J } ) ) = T )
52 50 51 sylib 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( { J } u. ( T \ { J } ) ) = T )
53 48 52 syl5eq 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( T \ { J } ) u. { J } ) = T )
54 53 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 } ) ) )
55 47 54 mpbid 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) : T --> ( S u. { y } ) )
56 ssidd 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> S C_ S )
57 snssi 
 |-  ( y e. S -> { y } C_ S )
58 57 ad2antrl 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> { y } C_ S )
59 56 58 unssd 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( S u. { y } ) C_ S )
60 55 59 fssd 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) : T --> S )
61 elmapex 
 |-  ( g e. ( S ^m ( T \ { J } ) ) -> ( S e. _V /\ ( T \ { J } ) e. _V ) )
62 61 ad2antll 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( S e. _V /\ ( T \ { J } ) e. _V ) )
63 62 simpld 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> S e. _V )
64 ssun1 
 |-  T C_ ( T u. { J } )
65 undif1 
 |-  ( ( T \ { J } ) u. { J } ) = ( T u. { J } )
66 62 simprd 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( T \ { J } ) e. _V )
67 snex 
 |-  { J } e. _V
68 unexg 
 |-  ( ( ( T \ { J } ) e. _V /\ { J } e. _V ) -> ( ( T \ { J } ) u. { J } ) e. _V )
69 66 67 68 sylancl 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( T \ { J } ) u. { J } ) e. _V )
70 65 69 eqeltrrid 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( T u. { J } ) e. _V )
71 ssexg 
 |-  ( ( T C_ ( T u. { J } ) /\ ( T u. { J } ) e. _V ) -> T e. _V )
72 64 70 71 sylancr 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> T e. _V )
73 63 72 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 ) )
74 60 73 mpbird 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) e. ( S ^m T ) )
75 eleq1 
 |-  ( f = ( g u. { <. J , y >. } ) -> ( f e. ( S ^m T ) <-> ( g u. { <. J , y >. } ) e. ( S ^m T ) ) )
76 74 75 syl5ibrcom 
 |-  ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( f = ( g u. { <. J , y >. } ) -> f e. ( S ^m T ) ) )
77 76 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 ) ) )
78 34 77 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 >. } ) ) )
79 1 adantl 
 |-  ( ( J e. T /\ f = ( g u. { <. J , y >. } ) ) -> ( ph <-> ps ) )
80 4 78 79 ralxpxfr2d 
 |-  ( J e. T -> ( A. f e. ( S ^m T ) ph <-> A. y e. S A. g e. ( S ^m ( T \ { J } ) ) ps ) )