Theorem dffv2 5951

Description: Alternate definition of function value df-fv 5606 that doesn't require dummy variables. (Contributed by NM, 4-Aug-2010.)

Assertion

Ref	Expression
dffv2	|- ( F ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )

Proof of Theorem dffv2

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		snidb 4023	. . . . 5 |- ( A e. _V <-> A e. { A } )
2		fvres 5892	. . . . 5 |- ( A e. { A } -> ( ( F |` { A } ) ` A ) = ( F ` A ) )
3	1, 2	sylbi 198	. . . 4 |- ( A e. _V -> ( ( F |` { A } ) ` A ) = ( F ` A ) )
4		fvprc 5872	. . . . 5 |- ( -. A e. _V -> ( ( F |` { A } ) ` A ) = (/) )
5		fvprc 5872	. . . . 5 |- ( -. A e. _V -> ( F ` A ) = (/) )
6	4, 5	eqtr4d 2466	. . . 4 |- ( -. A e. _V -> ( ( F |` { A } ) ` A ) = ( F ` A ) )
7	3, 6	pm2.61i 167	. . 3 |- ( ( F |` { A } ) ` A ) = ( F ` A )
8		funfv 5945	. . . 4 |- ( Fun ( F |` { A } ) -> ( ( F |` { A } ) ` A ) = U. ( ( F |` { A } ) " { A } ) )
9		df-fun 5600	. . . . . . . . . . . . 13 |- ( Fun ( F |` { A } ) <-> ( Rel ( F |` { A } ) /\ ( ( F |` { A } ) o. `' ( F |` { A } ) ) C_ _I ) )
10	9	simprbi 465	. . . . . . . . . . . 12 |- ( Fun ( F |` { A } ) -> ( ( F |` { A } ) o. `' ( F |` { A } ) ) C_ _I )
11		ssdif0 3851	. . . . . . . . . . . 12 |- ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) C_ _I <-> ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) = (/) )
12	10, 11	sylib 199	. . . . . . . . . . 11 |- ( Fun ( F |` { A } ) -> ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) = (/) )
13	12	unieqd 4226	. . . . . . . . . 10 |- ( Fun ( F |` { A } ) -> U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) = U. (/) )
14		uni0 4243	. . . . . . . . . 10 |- U. (/) = (/)
15	13, 14	syl6eq 2479	. . . . . . . . 9 |- ( Fun ( F |` { A } ) -> U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) = (/) )
16	15	unieqd 4226	. . . . . . . 8 |- ( Fun ( F |` { A } ) -> U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) = U. (/) )
17	16, 14	syl6eq 2479	. . . . . . 7 |- ( Fun ( F |` { A } ) -> U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) = (/) )
18	17	difeq2d 3583	. . . . . 6 |- ( Fun ( F |` { A } ) -> ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = ( ( F " { A } ) \ (/) ) )
19		resima 5153	. . . . . . 7 |- ( ( F |` { A } ) " { A } ) = ( F " { A } )
20		dif0 3865	. . . . . . 7 |- ( ( F " { A } ) \ (/) ) = ( F " { A } )
21	19, 20	eqtr4i 2454	. . . . . 6 |- ( ( F |` { A } ) " { A } ) = ( ( F " { A } ) \ (/) )
22	18, 21	syl6reqr 2482	. . . . 5 |- ( Fun ( F |` { A } ) -> ( ( F |` { A } ) " { A } ) = ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
23	22	unieqd 4226	. . . 4 |- ( Fun ( F |` { A } ) -> U. ( ( F |` { A } ) " { A } ) = U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
24	8, 23	eqtrd 2463	. . 3 |- ( Fun ( F |` { A } ) -> ( ( F |` { A } ) ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
25	7, 24	syl5eqr 2477	. 2 |- ( Fun ( F |` { A } ) -> ( F ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
26		nfunsn 5909	. . 3 |- ( -. Fun ( F |` { A } ) -> ( F ` A ) = (/) )
27		relres 5148	. . . . . . . . . . . . . . 15 |- Rel ( F |` { A } )
28		dffun3 5609	. . . . . . . . . . . . . . 15 |- ( Fun ( F |` { A } ) <-> ( Rel ( F |` { A } ) /\ A. x E. y A. z ( x ( F |` { A } ) z -> z = y ) ) )
29	27, 28	mpbiran 926	. . . . . . . . . . . . . 14 |- ( Fun ( F |` { A } ) <-> A. x E. y A. z ( x ( F |` { A } ) z -> z = y ) )
30		iman 425	. . . . . . . . . . . . . . . . . . 19 |- ( ( x ( F |` { A } ) z -> z = y ) <-> -. ( x ( F |` { A } ) z /\ -. z = y ) )
31	30	albii 1687	. . . . . . . . . . . . . . . . . 18 |- ( A. z ( x ( F |` { A } ) z -> z = y ) <-> A. z -. ( x ( F |` { A } ) z /\ -. z = y ) )
32		alnex 1661	. . . . . . . . . . . . . . . . . 18 |- ( A. z -. ( x ( F |` { A } ) z /\ -. z = y ) <-> -. E. z ( x ( F |` { A } ) z /\ -. z = y ) )
33	31, 32	bitri 252	. . . . . . . . . . . . . . . . 17 |- ( A. z ( x ( F |` { A } ) z -> z = y ) <-> -. E. z ( x ( F |` { A } ) z /\ -. z = y ) )
34	33	exbii 1712	. . . . . . . . . . . . . . . 16 |- ( E. y A. z ( x ( F |` { A } ) z -> z = y ) <-> E. y -. E. z ( x ( F |` { A } ) z /\ -. z = y ) )
35		exnal 1695	. . . . . . . . . . . . . . . 16 |- ( E. y -. E. z ( x ( F |` { A } ) z /\ -. z = y ) <-> -. A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) )
36	34, 35	bitri 252	. . . . . . . . . . . . . . 15 |- ( E. y A. z ( x ( F |` { A } ) z -> z = y ) <-> -. A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) )
37	36	albii 1687	. . . . . . . . . . . . . 14 |- ( A. x E. y A. z ( x ( F |` { A } ) z -> z = y ) <-> A. x -. A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) )
38		alnex 1661	. . . . . . . . . . . . . 14 |- ( A. x -. A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) <-> -. E. x A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) )
39	29, 37, 38	3bitrri 275	. . . . . . . . . . . . 13 |- ( -. E. x A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) <-> Fun ( F |` { A } ) )
40	39	con1bii 332	. . . . . . . . . . . 12 |- ( -. Fun ( F |` { A } ) <-> E. x A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) )
41		sp 1910	. . . . . . . . . . . . 13 |- ( A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) -> E. z ( x ( F |` { A } ) z /\ -. z = y ) )
42	41	eximi 1702	. . . . . . . . . . . 12 |- ( E. x A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) -> E. x E. z ( x ( F |` { A } ) z /\ -. z = y ) )
43	40, 42	sylbi 198	. . . . . . . . . . 11 |- ( -. Fun ( F |` { A } ) -> E. x E. z ( x ( F |` { A } ) z /\ -. z = y ) )
44		snssi 4141	. . . . . . . . . . . . . . . . . . . 20 |- ( A e. dom ( F |` { A } ) -> { A } C_ dom ( F |` { A } ) )
45		residm 5152	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( F |` { A } ) |` { A } ) = ( F |` { A } )
46	45	dmeqi 5052	. . . . . . . . . . . . . . . . . . . . 21 |- dom ( ( F |` { A } ) |` { A } ) = dom ( F |` { A } )
47		ssdmres 5142	. . . . . . . . . . . . . . . . . . . . . 22 |- ( { A } C_ dom ( F |` { A } ) <-> dom ( ( F |` { A } ) |` { A } ) = { A } )
48	47	biimpi 197	. . . . . . . . . . . . . . . . . . . . 21 |- ( { A } C_ dom ( F |` { A } ) -> dom ( ( F |` { A } ) |` { A } ) = { A } )
49	46, 48	syl5eqr 2477	. . . . . . . . . . . . . . . . . . . 20 |- ( { A } C_ dom ( F |` { A } ) -> dom ( F |` { A } ) = { A } )
50	44, 49	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( A e. dom ( F |` { A } ) -> dom ( F |` { A } ) = { A } )
51		vex 3084	. . . . . . . . . . . . . . . . . . . 20 |- x e. _V
52		vex 3084	. . . . . . . . . . . . . . . . . . . 20 |- z e. _V
53	51, 52	breldm 5055	. . . . . . . . . . . . . . . . . . 19 |- ( x ( F |` { A } ) z -> x e. dom ( F |` { A } ) )
54		eleq2 2495	. . . . . . . . . . . . . . . . . . . . 21 |- ( dom ( F |` { A } ) = { A } -> ( x e. dom ( F |` { A } ) <-> x e. { A } ) )
55		elsn 4010	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. { A } <-> x = A )
56	54, 55	syl6bb 264	. . . . . . . . . . . . . . . . . . . 20 |- ( dom ( F |` { A } ) = { A } -> ( x e. dom ( F |` { A } ) <-> x = A ) )
57	56	biimpa 486	. . . . . . . . . . . . . . . . . . 19 |- ( ( dom ( F |` { A } ) = { A } /\ x e. dom ( F |` { A } ) ) -> x = A )
58	50, 53, 57	syl2an 479	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. dom ( F |` { A } ) /\ x ( F |` { A } ) z ) -> x = A )
59	58	breq1d 4430	. . . . . . . . . . . . . . . . 17 |- ( ( A e. dom ( F |` { A } ) /\ x ( F |` { A } ) z ) -> ( x ( F |` { A } ) z <-> A ( F |` { A } ) z ) )
60	59	biimpd 210	. . . . . . . . . . . . . . . 16 |- ( ( A e. dom ( F |` { A } ) /\ x ( F |` { A } ) z ) -> ( x ( F |` { A } ) z -> A ( F |` { A } ) z ) )
61	60	ex 435	. . . . . . . . . . . . . . 15 |- ( A e. dom ( F |` { A } ) -> ( x ( F |` { A } ) z -> ( x ( F |` { A } ) z -> A ( F |` { A } ) z ) ) )
62	61	pm2.43d 50	. . . . . . . . . . . . . 14 |- ( A e. dom ( F |` { A } ) -> ( x ( F |` { A } ) z -> A ( F |` { A } ) z ) )
63	62	anim1d 566	. . . . . . . . . . . . 13 |- ( A e. dom ( F |` { A } ) -> ( ( x ( F |` { A } ) z /\ -. z = y ) -> ( A ( F |` { A } ) z /\ -. z = y ) ) )
64	63	eximdv 1754	. . . . . . . . . . . 12 |- ( A e. dom ( F |` { A } ) -> ( E. z ( x ( F |` { A } ) z /\ -. z = y ) -> E. z ( A ( F |` { A } ) z /\ -. z = y ) ) )
65	64	exlimdv 1768	. . . . . . . . . . 11 |- ( A e. dom ( F |` { A } ) -> ( E. x E. z ( x ( F |` { A } ) z /\ -. z = y ) -> E. z ( A ( F |` { A } ) z /\ -. z = y ) ) )
66	43, 65	mpan9 471	. . . . . . . . . 10 |- ( ( -. Fun ( F |` { A } ) /\ A e. dom ( F |` { A } ) ) -> E. z ( A ( F |` { A } ) z /\ -. z = y ) )
67	19	eleq2i 2500	. . . . . . . . . . . . 13 |- ( y e. ( ( F |` { A } ) " { A } ) <-> y e. ( F " { A } ) )
68		elimasni 5211	. . . . . . . . . . . . 13 |- ( y e. ( ( F |` { A } ) " { A } ) -> A ( F |` { A } ) y )
69	67, 68	sylbir 216	. . . . . . . . . . . 12 |- ( y e. ( F " { A } ) -> A ( F |` { A } ) y )
70		vex 3084	. . . . . . . . . . . . . . . . 17 |- y e. _V
71	70, 52	uniop 4720	. . . . . . . . . . . . . . . 16 |- U. <. y , z >. = { y , z }
72		opex 4682	. . . . . . . . . . . . . . . . . . 19 |- <. y , z >. e. _V
73	72	unisn 4231	. . . . . . . . . . . . . . . . . 18 |- U. { <. y , z >. } = <. y , z >.
74	27	brrelexi 4891	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A ( F |` { A } ) z -> A e. _V )
75		brcnvg 5031	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( y e. _V /\ A e. _V ) -> ( y `' ( F |` { A } ) A <-> A ( F |` { A } ) y ) )
76	70, 74, 75	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A ( F |` { A } ) z -> ( y `' ( F |` { A } ) A <-> A ( F |` { A } ) y ) )
77	76	biimpar 487	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A ( F |` { A } ) z /\ A ( F |` { A } ) y ) -> y `' ( F |` { A } ) A )
78	74	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( y `' ( F |` { A } ) A /\ A ( F |` { A } ) z ) -> A e. _V )
79		breq2 4424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x = A -> ( y `' ( F |` { A } ) x <-> y `' ( F |` { A } ) A ) )
80		breq1 4423	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x = A -> ( x ( F |` { A } ) z <-> A ( F |` { A } ) z ) )
81	79, 80	anbi12d 715	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x = A -> ( ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) <-> ( y `' ( F |` { A } ) A /\ A ( F |` { A } ) z ) ) )
82	81	rspcev 3182	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A e. _V /\ ( y `' ( F |` { A } ) A /\ A ( F |` { A } ) z ) ) -> E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) )
83	78, 82	mpancom 673	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( y `' ( F |` { A } ) A /\ A ( F |` { A } ) z ) -> E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) )
84	83	ancoms 454	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A ( F |` { A } ) z /\ y `' ( F |` { A } ) A ) -> E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) )
85	77, 84	syldan 472	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A ( F |` { A } ) z /\ A ( F |` { A } ) y ) -> E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) )
86	85	anim1i 570	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A ( F |` { A } ) z /\ A ( F |` { A } ) y ) /\ -. z = y ) -> ( E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) /\ -. z = y ) )
87	86	an32s 811	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> ( E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) /\ -. z = y ) )
88		eldif 3446	. . . . . . . . . . . . . . . . . . . . 21 |- ( <. y , z >. e. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) <-> ( <. y , z >. e. ( ( F |` { A } ) o. `' ( F |` { A } ) ) /\ -. <. y , z >. e. _I ) )
89		rexv 3096	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) <-> E. x ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) )
90	70, 52	brco 5021	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y ( ( F |` { A } ) o. `' ( F |` { A } ) ) z <-> E. x ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) )
91		df-br 4421	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y ( ( F |` { A } ) o. `' ( F |` { A } ) ) z <-> <. y , z >. e. ( ( F |` { A } ) o. `' ( F |` { A } ) ) )
92	89, 90, 91	3bitr2ri 277	. . . . . . . . . . . . . . . . . . . . . 22 |- ( <. y , z >. e. ( ( F |` { A } ) o. `' ( F |` { A } ) ) <-> E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) )
93	52	ideq 5003	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y _I z <-> y = z )
94		df-br 4421	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y _I z <-> <. y , z >. e. _I )
95		equcom 1844	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = z <-> z = y )
96	93, 94, 95	3bitr3i 278	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( <. y , z >. e. _I <-> z = y )
97	96	notbii 297	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. <. y , z >. e. _I <-> -. z = y )
98	92, 97	anbi12i 701	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( <. y , z >. e. ( ( F |` { A } ) o. `' ( F |` { A } ) ) /\ -. <. y , z >. e. _I ) <-> ( E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) /\ -. z = y ) )
99	88, 98	bitr2i 253	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) /\ -. z = y ) <-> <. y , z >. e. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
100	87, 99	sylib 199	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> <. y , z >. e. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
101		snssi 4141	. . . . . . . . . . . . . . . . . . 19 |- ( <. y , z >. e. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) -> { <. y , z >. } C_ ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
102		uniss 4237	. . . . . . . . . . . . . . . . . . 19 |- ( { <. y , z >. } C_ ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) -> U. { <. y , z >. } C_ U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
103	100, 101, 102	3syl 18	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> U. { <. y , z >. } C_ U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
104	73, 103	syl5eqssr 3509	. . . . . . . . . . . . . . . . 17 |- ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> <. y , z >. C_ U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
105	104	unissd 4240	. . . . . . . . . . . . . . . 16 |- ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> U. <. y , z >. C_ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
106	71, 105	syl5eqssr 3509	. . . . . . . . . . . . . . 15 |- ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> { y , z } C_ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
107	70, 52	prss 4151	. . . . . . . . . . . . . . 15 |- ( ( y e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) /\ z e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) <-> { y , z } C_ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
108	106, 107	sylibr 215	. . . . . . . . . . . . . 14 |- ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> ( y e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) /\ z e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
109	108	simpld 460	. . . . . . . . . . . . 13 |- ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> y e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
110	109	ex 435	. . . . . . . . . . . 12 |- ( ( A ( F |` { A } ) z /\ -. z = y ) -> ( A ( F |` { A } ) y -> y e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
111	69, 110	syl5 33	. . . . . . . . . . 11 |- ( ( A ( F |` { A } ) z /\ -. z = y ) -> ( y e. ( F " { A } ) -> y e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
112	111	exlimiv 1766	. . . . . . . . . 10 |- ( E. z ( A ( F |` { A } ) z /\ -. z = y ) -> ( y e. ( F " { A } ) -> y e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
113	66, 112	syl 17	. . . . . . . . 9 |- ( ( -. Fun ( F |` { A } ) /\ A e. dom ( F |` { A } ) ) -> ( y e. ( F " { A } ) -> y e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
114	113	ssrdv 3470	. . . . . . . 8 |- ( ( -. Fun ( F |` { A } ) /\ A e. dom ( F |` { A } ) ) -> ( F " { A } ) C_ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
115		ssdif0 3851	. . . . . . . 8 |- ( ( F " { A } ) C_ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) <-> ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = (/) )
116	114, 115	sylib 199	. . . . . . 7 |- ( ( -. Fun ( F |` { A } ) /\ A e. dom ( F |` { A } ) ) -> ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = (/) )
117	116	ex 435	. . . . . 6 |- ( -. Fun ( F |` { A } ) -> ( A e. dom ( F |` { A } ) -> ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = (/) ) )
118		ndmima 5221	. . . . . . . . 9 |- ( -. A e. dom ( F |` { A } ) -> ( ( F |` { A } ) " { A } ) = (/) )
119	19, 118	syl5eqr 2477	. . . . . . . 8 |- ( -. A e. dom ( F |` { A } ) -> ( F " { A } ) = (/) )
120	119	difeq1d 3582	. . . . . . 7 |- ( -. A e. dom ( F |` { A } ) -> ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = ( (/) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
121		0dif 3866	. . . . . . 7 |- ( (/) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = (/)
122	120, 121	syl6eq 2479	. . . . . 6 |- ( -. A e. dom ( F |` { A } ) -> ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = (/) )
123	117, 122	pm2.61d1 162	. . . . 5 |- ( -. Fun ( F |` { A } ) -> ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = (/) )
124	123	unieqd 4226	. . . 4 |- ( -. Fun ( F |` { A } ) -> U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = U. (/) )
125	124, 14	syl6eq 2479	. . 3 |- ( -. Fun ( F |` { A } ) -> U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = (/) )
126	26, 125	eqtr4d 2466	. 2 |- ( -. Fun ( F |` { A } ) -> ( F ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
127	25, 126	pm2.61i 167	1 |- ( F ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   A.wal 1435   = wceq 1437   E.wex 1659   e. wcel 1868   E.wrex 2776   _Vcvv 3081   \ cdif 3433   C_ wss 3436   (/)c0 3761   {csn 3996   {cpr 3998   <.cop 4002   U.cuni 4216   class class class wbr 4420   _I cid 4760   `'ccnv 4849   dom cdm 4850   |` cres 4852   "cima 4853   o. ccom 4854   Rel wrel 4855   Fun wfun 5592   ` cfv 5598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-fv 5606

This theorem is referenced by: (None)