dffv2

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

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

Proof

Step	Hyp	Ref	Expression
1		snidb	\|- ( A e. _V <-> A e. { A } )
2		fvres	\|- ( A e. { A } -> ( ( F \|` { A } ) ` A ) = ( F ` A ) )
3	1 2	sylbi	\|- ( A e. _V -> ( ( F \|` { A } ) ` A ) = ( F ` A ) )
4		fvprc	\|- ( -. A e. _V -> ( ( F \|` { A } ) ` A ) = (/) )
5		fvprc	\|- ( -. A e. _V -> ( F ` A ) = (/) )
6	4 5	eqtr4d	\|- ( -. A e. _V -> ( ( F \|` { A } ) ` A ) = ( F ` A ) )
7	3 6	pm2.61i	\|- ( ( F \|` { A } ) ` A ) = ( F ` A )
8		funfv	\|- ( Fun ( F \|` { A } ) -> ( ( F \|` { A } ) ` A ) = U. ( ( F \|` { A } ) " { A } ) )
9		resima	\|- ( ( F \|` { A } ) " { A } ) = ( F " { A } )
10		dif0	\|- ( ( F " { A } ) \ (/) ) = ( F " { A } )
11	9 10	eqtr4i	\|- ( ( F \|` { A } ) " { A } ) = ( ( F " { A } ) \ (/) )
12		df-fun	\|- ( Fun ( F \|` { A } ) <-> ( Rel ( F \|` { A } ) /\ ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) C_ _I ) )
13	12	simprbi	\|- ( Fun ( F \|` { A } ) -> ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) C_ _I )
14		ssdif0	\|- ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) C_ _I <-> ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) = (/) )
15	13 14	sylib	\|- ( Fun ( F \|` { A } ) -> ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) = (/) )
16	15	unieqd	\|- ( Fun ( F \|` { A } ) -> U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) = U. (/) )
17		uni0	\|- U. (/) = (/)
18	16 17	eqtrdi	\|- ( Fun ( F \|` { A } ) -> U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) = (/) )
19	18	unieqd	\|- ( Fun ( F \|` { A } ) -> U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) = U. (/) )
20	19 17	eqtrdi	\|- ( Fun ( F \|` { A } ) -> U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) = (/) )
21	20	difeq2d	\|- ( Fun ( F \|` { A } ) -> ( ( F " { A } ) \ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) = ( ( F " { A } ) \ (/) ) )
22	11 21	eqtr4id	\|- ( Fun ( F \|` { A } ) -> ( ( F \|` { A } ) " { A } ) = ( ( F " { A } ) \ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) )
23	22	unieqd	\|- ( Fun ( F \|` { A } ) -> U. ( ( F \|` { A } ) " { A } ) = U. ( ( F " { A } ) \ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) )
24	8 23	eqtrd	\|- ( Fun ( F \|` { A } ) -> ( ( F \|` { A } ) ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) )
25	7 24	eqtr3id	\|- ( Fun ( F \|` { A } ) -> ( F ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) )
26		nfunsn	\|- ( -. Fun ( F \|` { A } ) -> ( F ` A ) = (/) )
27		relres	\|- Rel ( F \|` { A } )
28		dffun3	\|- ( Fun ( F \|` { A } ) <-> ( Rel ( F \|` { A } ) /\ A. x E. y A. z ( x ( F \|` { A } ) z -> z = y ) ) )
29	27 28	mpbiran	\|- ( Fun ( F \|` { A } ) <-> A. x E. y A. z ( x ( F \|` { A } ) z -> z = y ) )
30		iman	\|- ( ( x ( F \|` { A } ) z -> z = y ) <-> -. ( x ( F \|` { A } ) z /\ -. z = y ) )
31	30	albii	\|- ( A. z ( x ( F \|` { A } ) z -> z = y ) <-> A. z -. ( x ( F \|` { A } ) z /\ -. z = y ) )
32		alnex	\|- ( A. z -. ( x ( F \|` { A } ) z /\ -. z = y ) <-> -. E. z ( x ( F \|` { A } ) z /\ -. z = y ) )
33	31 32	bitri	\|- ( A. z ( x ( F \|` { A } ) z -> z = y ) <-> -. E. z ( x ( F \|` { A } ) z /\ -. z = y ) )
34	33	exbii	\|- ( E. y A. z ( x ( F \|` { A } ) z -> z = y ) <-> E. y -. E. z ( x ( F \|` { A } ) z /\ -. z = y ) )
35		exnal	\|- ( E. y -. E. z ( x ( F \|` { A } ) z /\ -. z = y ) <-> -. A. y E. z ( x ( F \|` { A } ) z /\ -. z = y ) )
36	34 35	bitri	\|- ( E. y A. z ( x ( F \|` { A } ) z -> z = y ) <-> -. A. y E. z ( x ( F \|` { A } ) z /\ -. z = y ) )
37	36	albii	\|- ( 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	\|- ( 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	\|- ( -. E. x A. y E. z ( x ( F \|` { A } ) z /\ -. z = y ) <-> Fun ( F \|` { A } ) )
40	39	con1bii	\|- ( -. Fun ( F \|` { A } ) <-> E. x A. y E. z ( x ( F \|` { A } ) z /\ -. z = y ) )
41		sp	\|- ( A. y E. z ( x ( F \|` { A } ) z /\ -. z = y ) -> E. z ( x ( F \|` { A } ) z /\ -. z = y ) )
42	41	eximi	\|- ( 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	\|- ( -. Fun ( F \|` { A } ) -> E. x E. z ( x ( F \|` { A } ) z /\ -. z = y ) )
44		snssi	\|- ( A e. dom ( F \|` { A } ) -> { A } C_ dom ( F \|` { A } ) )
45		residm	\|- ( ( F \|` { A } ) \|` { A } ) = ( F \|` { A } )
46	45	dmeqi	\|- dom ( ( F \|` { A } ) \|` { A } ) = dom ( F \|` { A } )
47		ssdmres	\|- ( { A } C_ dom ( F \|` { A } ) <-> dom ( ( F \|` { A } ) \|` { A } ) = { A } )
48	47	biimpi	\|- ( { A } C_ dom ( F \|` { A } ) -> dom ( ( F \|` { A } ) \|` { A } ) = { A } )
49	46 48	eqtr3id	\|- ( { A } C_ dom ( F \|` { A } ) -> dom ( F \|` { A } ) = { A } )
50	44 49	syl	\|- ( A e. dom ( F \|` { A } ) -> dom ( F \|` { A } ) = { A } )
51		vex	\|- x e. _V
52		vex	\|- z e. _V
53	51 52	breldm	\|- ( x ( F \|` { A } ) z -> x e. dom ( F \|` { A } ) )
54		eleq2	\|- ( dom ( F \|` { A } ) = { A } -> ( x e. dom ( F \|` { A } ) <-> x e. { A } ) )
55		velsn	\|- ( x e. { A } <-> x = A )
56	54 55	bitrdi	\|- ( dom ( F \|` { A } ) = { A } -> ( x e. dom ( F \|` { A } ) <-> x = A ) )
57	56	biimpa	\|- ( ( dom ( F \|` { A } ) = { A } /\ x e. dom ( F \|` { A } ) ) -> x = A )
58	50 53 57	syl2an	\|- ( ( A e. dom ( F \|` { A } ) /\ x ( F \|` { A } ) z ) -> x = A )
59	58	breq1d	\|- ( ( A e. dom ( F \|` { A } ) /\ x ( F \|` { A } ) z ) -> ( x ( F \|` { A } ) z <-> A ( F \|` { A } ) z ) )
60	59	biimpd	\|- ( ( A e. dom ( F \|` { A } ) /\ x ( F \|` { A } ) z ) -> ( x ( F \|` { A } ) z -> A ( F \|` { A } ) z ) )
61	60	ex	\|- ( A e. dom ( F \|` { A } ) -> ( x ( F \|` { A } ) z -> ( x ( F \|` { A } ) z -> A ( F \|` { A } ) z ) ) )
62	61	pm2.43d	\|- ( A e. dom ( F \|` { A } ) -> ( x ( F \|` { A } ) z -> A ( F \|` { A } ) z ) )
63	62	anim1d	\|- ( A e. dom ( F \|` { A } ) -> ( ( x ( F \|` { A } ) z /\ -. z = y ) -> ( A ( F \|` { A } ) z /\ -. z = y ) ) )
64	63	eximdv	\|- ( A e. dom ( F \|` { A } ) -> ( E. z ( x ( F \|` { A } ) z /\ -. z = y ) -> E. z ( A ( F \|` { A } ) z /\ -. z = y ) ) )
65	64	exlimdv	\|- ( 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	\|- ( ( -. Fun ( F \|` { A } ) /\ A e. dom ( F \|` { A } ) ) -> E. z ( A ( F \|` { A } ) z /\ -. z = y ) )
67	9	eleq2i	\|- ( y e. ( ( F \|` { A } ) " { A } ) <-> y e. ( F " { A } ) )
68		elimasni	\|- ( y e. ( ( F \|` { A } ) " { A } ) -> A ( F \|` { A } ) y )
69	67 68	sylbir	\|- ( y e. ( F " { A } ) -> A ( F \|` { A } ) y )
70		vex	\|- y e. _V
71	70 52	uniop	\|- U. <. y , z >. = { y , z }
72		opex	\|- <. y , z >. e. _V
73	72	unisn	\|- U. { <. y , z >. } = <. y , z >.
74	27	brrelex1i	\|- ( A ( F \|` { A } ) z -> A e. _V )
75		brcnvg	\|- ( ( y e. _V /\ A e. _V ) -> ( y `' ( F \|` { A } ) A <-> A ( F \|` { A } ) y ) )
76	70 74 75	sylancr	\|- ( A ( F \|` { A } ) z -> ( y `' ( F \|` { A } ) A <-> A ( F \|` { A } ) y ) )
77	76	biimpar	\|- ( ( A ( F \|` { A } ) z /\ A ( F \|` { A } ) y ) -> y `' ( F \|` { A } ) A )
78	74	adantl	\|- ( ( y `' ( F \|` { A } ) A /\ A ( F \|` { A } ) z ) -> A e. _V )
79		breq2	\|- ( x = A -> ( y `' ( F \|` { A } ) x <-> y `' ( F \|` { A } ) A ) )
80		breq1	\|- ( x = A -> ( x ( F \|` { A } ) z <-> A ( F \|` { A } ) z ) )
81	79 80	anbi12d	\|- ( x = A -> ( ( y `' ( F \|` { A } ) x /\ x ( F \|` { A } ) z ) <-> ( y `' ( F \|` { A } ) A /\ A ( F \|` { A } ) z ) ) )
82	81	rspcev	\|- ( ( 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	\|- ( ( y `' ( F \|` { A } ) A /\ A ( F \|` { A } ) z ) -> E. x e. _V ( y `' ( F \|` { A } ) x /\ x ( F \|` { A } ) z ) )
84	83	ancoms	\|- ( ( A ( F \|` { A } ) z /\ y `' ( F \|` { A } ) A ) -> E. x e. _V ( y `' ( F \|` { A } ) x /\ x ( F \|` { A } ) z ) )
85	77 84	syldan	\|- ( ( A ( F \|` { A } ) z /\ A ( F \|` { A } ) y ) -> E. x e. _V ( y `' ( F \|` { A } ) x /\ x ( F \|` { A } ) z ) )
86	85	anim1i	\|- ( ( ( 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	\|- ( ( ( 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	\|- ( <. y , z >. e. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) <-> ( <. y , z >. e. ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) /\ -. <. y , z >. e. _I ) )
89		rexv	\|- ( 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	\|- ( y ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) z <-> E. x ( y `' ( F \|` { A } ) x /\ x ( F \|` { A } ) z ) )
91		df-br	\|- ( y ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) z <-> <. y , z >. e. ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) )
92	89 90 91	3bitr2ri	\|- ( <. y , z >. e. ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) <-> E. x e. _V ( y `' ( F \|` { A } ) x /\ x ( F \|` { A } ) z ) )
93	52	ideq	\|- ( y _I z <-> y = z )
94		df-br	\|- ( y _I z <-> <. y , z >. e. _I )
95		equcom	\|- ( y = z <-> z = y )
96	93 94 95	3bitr3i	\|- ( <. y , z >. e. _I <-> z = y )
97	96	notbii	\|- ( -. <. y , z >. e. _I <-> -. z = y )
98	92 97	anbi12i	\|- ( ( <. 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	\|- ( ( 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	\|- ( ( ( A ( F \|` { A } ) z /\ -. z = y ) /\ A ( F \|` { A } ) y ) -> <. y , z >. e. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) )
101		snssi	\|- ( <. y , z >. e. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) -> { <. y , z >. } C_ ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) )
102		uniss	\|- ( { <. 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	\|- ( ( ( A ( F \|` { A } ) z /\ -. z = y ) /\ A ( F \|` { A } ) y ) -> U. { <. y , z >. } C_ U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) )
104	73 103	eqsstrrid	\|- ( ( ( A ( F \|` { A } ) z /\ -. z = y ) /\ A ( F \|` { A } ) y ) -> <. y , z >. C_ U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) )
105	104	unissd	\|- ( ( ( 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	eqsstrrid	\|- ( ( ( 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	\|- ( ( 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	\|- ( ( ( 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	\|- ( ( ( A ( F \|` { A } ) z /\ -. z = y ) /\ A ( F \|` { A } ) y ) -> y e. U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) )
110	109	ex	\|- ( ( A ( F \|` { A } ) z /\ -. z = y ) -> ( A ( F \|` { A } ) y -> y e. U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) )
111	69 110	syl5	\|- ( ( A ( F \|` { A } ) z /\ -. z = y ) -> ( y e. ( F " { A } ) -> y e. U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) )
112	111	exlimiv	\|- ( 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	\|- ( ( -. 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	\|- ( ( -. Fun ( F \|` { A } ) /\ A e. dom ( F \|` { A } ) ) -> ( F " { A } ) C_ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) )
115		ssdif0	\|- ( ( 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	\|- ( ( -. Fun ( F \|` { A } ) /\ A e. dom ( F \|` { A } ) ) -> ( ( F " { A } ) \ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) = (/) )
117	116	ex	\|- ( -. Fun ( F \|` { A } ) -> ( A e. dom ( F \|` { A } ) -> ( ( F " { A } ) \ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) = (/) ) )
118		ndmima	\|- ( -. A e. dom ( F \|` { A } ) -> ( ( F \|` { A } ) " { A } ) = (/) )
119	9 118	eqtr3id	\|- ( -. A e. dom ( F \|` { A } ) -> ( F " { A } ) = (/) )
120	119	difeq1d	\|- ( -. 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	\|- ( (/) \ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) = (/)
122	120 121	eqtrdi	\|- ( -. A e. dom ( F \|` { A } ) -> ( ( F " { A } ) \ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) = (/) )
123	117 122	pm2.61d1	\|- ( -. Fun ( F \|` { A } ) -> ( ( F " { A } ) \ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) = (/) )
124	123	unieqd	\|- ( -. Fun ( F \|` { A } ) -> U. ( ( F " { A } ) \ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) = U. (/) )
125	124 17	eqtrdi	\|- ( -. Fun ( F \|` { A } ) -> U. ( ( F " { A } ) \ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) = (/) )
126	26 125	eqtr4d	\|- ( -. Fun ( F \|` { A } ) -> ( F ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) ) )
127	25 126	pm2.61i	\|- ( F ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F \|` { A } ) o. `' ( F \|` { A } ) ) \ _I ) )

Metamath Proof Explorer

Theorem dffv2

Proof