Theorem ralxpmap 7907

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.)

Hypothesis

Ref	Expression
ralxpmap.j	|- ( f = ( g u. { <. J , y >. } ) -> ( ph <-> ps ) )

Assertion

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

Distinct variable groups:   ph, g, y   ps, f   f, J, g, y   S, f, g, y   T, f, g, y

Allowed substitution hints:   ph( f)   ps( y, g)

Proof of Theorem ralxpmap

Step	Hyp	Ref	Expression
1		vex 3203	. . 3 |- g e. _V
2		snex 4908	. . 3 |- { <. J , y >. } e. _V
3	1, 2	unex 6956	. 2 |- ( g u. { <. J , y >. } ) e. _V
4		simpr 477	. . . . . . 7 |- ( ( J e. T /\ f e. ( S ^m T ) ) -> f e. ( S ^m T ) )
5		elmapex 7878	. . . . . . . . 9 |- ( f e. ( S ^m T ) -> ( S e. _V /\ T e. _V ) )
6	5	adantl 482	. . . . . . . 8 |- ( ( J e. T /\ f e. ( S ^m T ) ) -> ( S e. _V /\ T e. _V ) )
7		elmapg 7870	. . . . . . . 8 |- ( ( S e. _V /\ T e. _V ) -> ( f e. ( S ^m T ) <-> f : T --> S ) )
8	6, 7	syl 17	. . . . . . 7 |- ( ( J e. T /\ f e. ( S ^m T ) ) -> ( f e. ( S ^m T ) <-> f : T --> S ) )
9	4, 8	mpbid 222	. . . . . 6 |- ( ( J e. T /\ f e. ( S ^m T ) ) -> f : T --> S )
10		simpl 473	. . . . . 6 |- ( ( J e. T /\ f e. ( S ^m T ) ) -> J e. T )
11	9, 10	ffvelrnd 6360	. . . . 5 |- ( ( J e. T /\ f e. ( S ^m T ) ) -> ( f ` J ) e. S )
12		difss 3737	. . . . . . 7 |- ( T \ { J } ) C_ T
13		fssres 6070	. . . . . . 7 |- ( ( f : T --> S /\ ( T \ { J } ) C_ T ) -> ( f |` ( T \ { J } ) ) : ( T \ { J } ) --> S )
14	9, 12, 13	sylancl 694	. . . . . 6 |- ( ( J e. T /\ f e. ( S ^m T ) ) -> ( f |` ( T \ { J } ) ) : ( T \ { J } ) --> S )
15	5	simpld 475	. . . . . . . 8 |- ( f e. ( S ^m T ) -> S e. _V )
16	15	adantl 482	. . . . . . 7 |- ( ( J e. T /\ f e. ( S ^m T ) ) -> S e. _V )
17	6	simprd 479	. . . . . . . 8 |- ( ( J e. T /\ f e. ( S ^m T ) ) -> T e. _V )
18		difexg 4808	. . . . . . . 8 |- ( T e. _V -> ( T \ { J } ) e. _V )
19	17, 18	syl 17	. . . . . . 7 |- ( ( J e. T /\ f e. ( S ^m T ) ) -> ( T \ { J } ) e. _V )
20	16, 19	elmapd 7871	. . . . . 6 |- ( ( J e. T /\ f e. ( S ^m T ) ) -> ( ( f |` ( T \ { J } ) ) e. ( S ^m ( T \ { J } ) ) <-> ( f |` ( T \ { J } ) ) : ( T \ { J } ) --> S ) )
21	14, 20	mpbird 247	. . . . 5 |- ( ( J e. T /\ f e. ( S ^m T ) ) -> ( f |` ( T \ { J } ) ) e. ( S ^m ( T \ { J } ) ) )
22		ffn 6045	. . . . . . 7 |- ( f : T --> S -> f Fn T )
23	9, 22	syl 17	. . . . . 6 |- ( ( J e. T /\ f e. ( S ^m T ) ) -> f Fn T )
24		fnsnsplit 6450	. . . . . 6 |- ( ( f Fn T /\ J e. T ) -> f = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) )
25	23, 10, 24	syl2anc 693	. . . . 5 |- ( ( J e. T /\ f e. ( S ^m T ) ) -> f = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) )
26		opeq2 4403	. . . . . . . . 9 |- ( y = ( f ` J ) -> <. J , y >. = <. J , ( f ` J ) >. )
27	26	sneqd 4189	. . . . . . . 8 |- ( y = ( f ` J ) -> { <. J , y >. } = { <. J , ( f ` J ) >. } )
28	27	uneq2d 3767	. . . . . . 7 |- ( y = ( f ` J ) -> ( g u. { <. J , y >. } ) = ( g u. { <. J , ( f ` J ) >. } ) )
29	28	eqeq2d 2632	. . . . . 6 |- ( y = ( f ` J ) -> ( f = ( g u. { <. J , y >. } ) <-> f = ( g u. { <. J , ( f ` J ) >. } ) ) )
30		uneq1 3760	. . . . . . 7 |- ( g = ( f |` ( T \ { J } ) ) -> ( g u. { <. J , ( f ` J ) >. } ) = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) )
31	30	eqeq2d 2632	. . . . . 6 |- ( g = ( f |` ( T \ { J } ) ) -> ( f = ( g u. { <. J , ( f ` J ) >. } ) <-> f = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) ) )
32	29, 31	rspc2ev 3324	. . . . 5 |- ( ( ( 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	11, 21, 25, 32	syl3anc 1326	. . . 4 |- ( ( 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 450	. . 3 |- ( 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 7879	. . . . . . . . . 10 |- ( g e. ( S ^m ( T \ { J } ) ) -> g : ( T \ { J } ) --> S )
36	35	ad2antll 765	. . . . . . . . 9 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> g : ( T \ { J } ) --> S )
37		vex 3203	. . . . . . . . . . 11 |- y e. _V
38		f1osng 6177	. . . . . . . . . . . 12 |- ( ( J e. T /\ y e. _V ) -> { <. J , y >. } : { J } -1-1-onto-> { y } )
39		f1of 6137	. . . . . . . . . . . 12 |- ( { <. J , y >. } : { J } -1-1-onto-> { y } -> { <. J , y >. } : { J } --> { y } )
40	38, 39	syl 17	. . . . . . . . . . 11 |- ( ( J e. T /\ y e. _V ) -> { <. J , y >. } : { J } --> { y } )
41	37, 40	mpan2 707	. . . . . . . . . 10 |- ( J e. T -> { <. J , y >. } : { J } --> { y } )
42	41	adantr 481	. . . . . . . . 9 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> { <. J , y >. } : { J } --> { y } )
43		incom 3805	. . . . . . . . . . 11 |- ( ( T \ { J } ) i^i { J } ) = ( { J } i^i ( T \ { J } ) )
44		disjdif 4040	. . . . . . . . . . 11 |- ( { J } i^i ( T \ { J } ) ) = (/)
45	43, 44	eqtri 2644	. . . . . . . . . 10 |- ( ( T \ { J } ) i^i { J } ) = (/)
46	45	a1i 11	. . . . . . . . 9 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( T \ { J } ) i^i { J } ) = (/) )
47		fun 6066	. . . . . . . . 9 |- ( ( ( g : ( T \ { J } ) --> S /\ { <. J , y >. } : { J } --> { y } ) /\ ( ( T \ { J } ) i^i { J } ) = (/) ) -> ( g u. { <. J , y >. } ) : ( ( T \ { J } ) u. { J } ) --> ( S u. { y } ) )
48	36, 42, 46, 47	syl21anc 1325	. . . . . . . 8 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) : ( ( T \ { J } ) u. { J } ) --> ( S u. { y } ) )
49		uncom 3757	. . . . . . . . . 10 |- ( ( T \ { J } ) u. { J } ) = ( { J } u. ( T \ { J } ) )
50		simpl 473	. . . . . . . . . . . 12 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> J e. T )
51	50	snssd 4340	. . . . . . . . . . 11 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> { J } C_ T )
52		undif 4049	. . . . . . . . . . 11 |- ( { J } C_ T <-> ( { J } u. ( T \ { J } ) ) = T )
53	51, 52	sylib 208	. . . . . . . . . 10 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( { J } u. ( T \ { J } ) ) = T )
54	49, 53	syl5eq 2668	. . . . . . . . 9 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( T \ { J } ) u. { J } ) = T )
55	54	feq2d 6031	. . . . . . . 8 |- ( ( 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 } ) ) )
56	48, 55	mpbid 222	. . . . . . 7 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) : T --> ( S u. { y } ) )
57		ssid 3624	. . . . . . . . 9 |- S C_ S
58	57	a1i 11	. . . . . . . 8 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> S C_ S )
59		snssi 4339	. . . . . . . . 9 |- ( y e. S -> { y } C_ S )
60	59	ad2antrl 764	. . . . . . . 8 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> { y } C_ S )
61	58, 60	unssd 3789	. . . . . . 7 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( S u. { y } ) C_ S )
62	56, 61	fssd 6057	. . . . . 6 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) : T --> S )
63		elmapex 7878	. . . . . . . . 9 |- ( g e. ( S ^m ( T \ { J } ) ) -> ( S e. _V /\ ( T \ { J } ) e. _V ) )
64	63	ad2antll 765	. . . . . . . 8 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( S e. _V /\ ( T \ { J } ) e. _V ) )
65	64	simpld 475	. . . . . . 7 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> S e. _V )
66		ssun1 3776	. . . . . . . 8 |- T C_ ( T u. { J } )
67		undif1 4043	. . . . . . . . 9 |- ( ( T \ { J } ) u. { J } ) = ( T u. { J } )
68	64	simprd 479	. . . . . . . . . 10 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( T \ { J } ) e. _V )
69		snex 4908	. . . . . . . . . 10 |- { J } e. _V
70		unexg 6959	. . . . . . . . . 10 |- ( ( ( T \ { J } ) e. _V /\ { J } e. _V ) -> ( ( T \ { J } ) u. { J } ) e. _V )
71	68, 69, 70	sylancl 694	. . . . . . . . 9 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( T \ { J } ) u. { J } ) e. _V )
72	67, 71	syl5eqelr 2706	. . . . . . . 8 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( T u. { J } ) e. _V )
73		ssexg 4804	. . . . . . . 8 |- ( ( T C_ ( T u. { J } ) /\ ( T u. { J } ) e. _V ) -> T e. _V )
74	66, 72, 73	sylancr 695	. . . . . . 7 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> T e. _V )
75	65, 74	elmapd 7871	. . . . . 6 |- ( ( 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 ) )
76	62, 75	mpbird 247	. . . . 5 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) e. ( S ^m T ) )
77		eleq1 2689	. . . . 5 |- ( f = ( g u. { <. J , y >. } ) -> ( f e. ( S ^m T ) <-> ( g u. { <. J , y >. } ) e. ( S ^m T ) ) )
78	76, 77	syl5ibrcom 237	. . . 4 |- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( f = ( g u. { <. J , y >. } ) -> f e. ( S ^m T ) ) )
79	78	rexlimdvva 3038	. . 3 |- ( J e. T -> ( E. y e. S E. g e. ( S ^m ( T \ { J } ) ) f = ( g u. { <. J , y >. } ) -> f e. ( S ^m T ) ) )
80	34, 79	impbid 202	. 2 |- ( J e. T -> ( f e. ( S ^m T ) <-> E. y e. S E. g e. ( S ^m ( T \ { J } ) ) f = ( g u. { <. J , y >. } ) ) )
81		ralxpmap.j	. . 3 |- ( f = ( g u. { <. J , y >. } ) -> ( ph <-> ps ) )
82	81	adantl 482	. 2 |- ( ( J e. T /\ f = ( g u. { <. J , y >. } ) ) -> ( ph <-> ps ) )
83	3, 80, 82	ralxpxfr2d 3327	1 |- ( J e. T -> ( A. f e. ( S ^m T ) ph <-> A. y e. S A. g e. ( S ^m ( T \ { J } ) ) ps ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   {csn 4177   <.cop 4183   |` cres 5116   Fn wfn 5883   -->wf 5884   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   ^m cmap 7857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-map 7859

This theorem is referenced by:  islindf4  20177