Theorem ralxpmap 7488

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

Assertion

Ref	Expression
ralxpmap

Distinct variable groups:   ,,   ,   ,J,,   S,,,   ,,,

Proof of Theorem ralxpmap

Step	Hyp	Ref	Expression
1		vex 3112	. . 3
2		snex 4693	. . 3
3	1, 2	unex 6598	. 2
4		simpr 461	. . . . . . 7
5		elmapex 7459	. . . . . . . . 9
6	5	adantl 466	. . . . . . . 8
7		elmapg 7452	. . . . . . . 8
8	6, 7	syl 16	. . . . . . 7
9	4, 8	mpbid 210	. . . . . 6
10		simpl 457	. . . . . 6
11	9, 10	ffvelrnd 6032	. . . . 5
12		difss 3630	. . . . . . 7
13		fssres 5756	. . . . . . 7
14	9, 12, 13	sylancl 662	. . . . . 6
15	5	simpld 459	. . . . . . . 8
16	15	adantl 466	. . . . . . 7
17	6	simprd 463	. . . . . . . 8
18		difexg 4600	. . . . . . . 8
19	17, 18	syl 16	. . . . . . 7
20	16, 19	elmapd 7453	. . . . . 6
21	14, 20	mpbird 232	. . . . 5
22		ffn 5736	. . . . . . 7
23	9, 22	syl 16	. . . . . 6
24		fnsnsplit 6108	. . . . . 6
25	23, 10, 24	syl2anc 661	. . . . 5
26		opeq2 4218	. . . . . . . . 9
27	26	sneqd 4041	. . . . . . . 8
28	27	uneq2d 3657	. . . . . . 7
29	28	eqeq2d 2471	. . . . . 6
30		uneq1 3650	. . . . . . 7
31	30	eqeq2d 2471	. . . . . 6
32	29, 31	rspc2ev 3221	. . . . 5
33	11, 21, 25, 32	syl3anc 1228	. . . 4
34	33	ex 434	. . 3
35		elmapi 7460	. . . . . . . . . 10
36	35	ad2antll 728	. . . . . . . . 9
37		vex 3112	. . . . . . . . . . 11
38		f1osng 5859	. . . . . . . . . . . 12
39		f1of 5821	. . . . . . . . . . . 12
40	38, 39	syl 16	. . . . . . . . . . 11
41	37, 40	mpan2 671	. . . . . . . . . 10
42	41	adantr 465	. . . . . . . . 9
43		incom 3690	. . . . . . . . . . 11
44		disjdif 3900	. . . . . . . . . . 11
45	43, 44	eqtri 2486	. . . . . . . . . 10
46	45	a1i 11	. . . . . . . . 9
47		fun 5753	. . . . . . . . 9
48	36, 42, 46, 47	syl21anc 1227	. . . . . . . 8
49		uncom 3647	. . . . . . . . . 10
50		simpl 457	. . . . . . . . . . . 12
51	50	snssd 4175	. . . . . . . . . . 11
52		undif 3908	. . . . . . . . . . 11
53	51, 52	sylib 196	. . . . . . . . . 10
54	49, 53	syl5eq 2510	. . . . . . . . 9
55	54	feq2d 5723	. . . . . . . 8
56	48, 55	mpbid 210	. . . . . . 7
57		ssid 3522	. . . . . . . . 9
58	57	a1i 11	. . . . . . . 8
59		snssi 4174	. . . . . . . . 9
60	59	ad2antrl 727	. . . . . . . 8
61	58, 60	unssd 3679	. . . . . . 7
62	56, 61	fssd 5745	. . . . . 6
63		elmapex 7459	. . . . . . . . 9
64	63	ad2antll 728	. . . . . . . 8
65	64	simpld 459	. . . . . . 7
66		ssun1 3666	. . . . . . . 8
67		undif1 3903	. . . . . . . . 9
68	64	simprd 463	. . . . . . . . . 10
69		snex 4693	. . . . . . . . . 10
70		unexg 6601	. . . . . . . . . 10
71	68, 69, 70	sylancl 662	. . . . . . . . 9
72	67, 71	syl5eqelr 2550	. . . . . . . 8
73		ssexg 4598	. . . . . . . 8
74	66, 72, 73	sylancr 663	. . . . . . 7
75	65, 74	elmapd 7453	. . . . . 6
76	62, 75	mpbird 232	. . . . 5
77		eleq1 2529	. . . . 5
78	76, 77	syl5ibrcom 222	. . . 4
79	78	rexlimdvva 2956	. . 3
80	34, 79	impbid 191	. 2
81		ralxpmap.j	. . 3
82	81	adantl 466	. 2
83	3, 80, 82	ralxpxfr2d 3224	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807  E.wrex 2808  cvv 3109  \cdif 3472  u.cun 3473  i^icin 3474  C_wss 3475  c0 3784  {csn 4029  <.cop 4035  |`cres 5006  Fnwfn 5588  -->wf 5589  -1-1-onto->wf1o 5592  `cfv 5593  (class class class)co 6296  cmap 7439

This theorem is referenced by:  islindf4  18873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-1st 6800  df-2nd 6801  df-map 7441