Theorem brapply 32045

Description: Binary relation form of the Apply function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)

Hypotheses

Ref	Expression
brapply.1	|- A e. _V
brapply.2	|- B e. _V
brapply.3	|- C e. _V

Assertion

Ref	Expression
brapply	|- ( <. A , B >.Apply C <-> C = ( A ` B ) )

Proof of Theorem brapply

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

Step	Hyp	Ref	Expression
1		snex 4908	. . . 4 |- { ( A " { B } ) } e. _V
2	1	inex1 4799	. . 3 |- ( { ( A " { B } ) } i^i Singletons ) e. _V
3		unieq 4444	. . . . 5 |- ( x = ( { ( A " { B } ) } i^i Singletons ) -> U. x = U. ( { ( A " { B } ) } i^i Singletons ) )
4	3	unieqd 4446	. . . 4 |- ( x = ( { ( A " { B } ) } i^i Singletons ) -> U. U. x = U. U. ( { ( A " { B } ) } i^i Singletons ) )
5	4	eqeq2d 2632	. . 3 |- ( x = ( { ( A " { B } ) } i^i Singletons ) -> ( C = U. U. x <-> C = U. U. ( { ( A " { B } ) } i^i Singletons ) ) )
6	2, 5	ceqsexv 3242	. 2 |- ( E. x ( x = ( { ( A " { B } ) } i^i Singletons ) /\ C = U. U. x ) <-> C = U. U. ( { ( A " { B } ) } i^i Singletons ) )
7		df-apply 31980	. . . 4 |- Apply = ( ( Bigcup o. Bigcup ) o. ( ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) o. ( (Singleton o. Img ) o. pprod ( _I , Singleton ) ) ) )
8	7	breqi 4659	. . 3 |- ( <. A , B >.Apply C <-> <. A , B >. ( ( Bigcup o. Bigcup ) o. ( ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) o. ( (Singleton o. Img ) o. pprod ( _I , Singleton ) ) ) ) C )
9		opex 4932	. . . 4 |- <. A , B >. e. _V
10		brapply.3	. . . 4 |- C e. _V
11	9, 10	brco 5292	. . 3 |- ( <. A , B >. ( ( Bigcup o. Bigcup ) o. ( ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) o. ( (Singleton o. Img ) o. pprod ( _I , Singleton ) ) ) ) C <-> E. x ( <. A , B >. ( ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) o. ( (Singleton o. Img ) o. pprod ( _I , Singleton ) ) ) x /\ x ( Bigcup o. Bigcup ) C ) )
12		vex 3203	. . . . . . 7 |- x e. _V
13	9, 12	brco 5292	. . . . . 6 |- ( <. A , B >. ( ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) o. ( (Singleton o. Img ) o. pprod ( _I , Singleton ) ) ) x <-> E. y ( <. A , B >. ( (Singleton o. Img ) o. pprod ( _I , Singleton ) ) y /\ y ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) x ) )
14		vex 3203	. . . . . . . . . 10 |- y e. _V
15	9, 14	brco 5292	. . . . . . . . 9 |- ( <. A , B >. ( (Singleton o. Img ) o. pprod ( _I , Singleton ) ) y <-> E. z ( <. A , B >.pprod ( _I , Singleton ) z /\ z (Singleton o. Img ) y ) )
16		brapply.1	. . . . . . . . . . . . 13 |- A e. _V
17		brapply.2	. . . . . . . . . . . . 13 |- B e. _V
18		vex 3203	. . . . . . . . . . . . 13 |- z e. _V
19	16, 17, 18	brpprod3a 31993	. . . . . . . . . . . 12 |- ( <. A , B >.pprod ( _I , Singleton ) z <-> E. a E. b ( z = <. a , b >. /\ A _I a /\ BSingleton b ) )
20		3anrot 1043	. . . . . . . . . . . . . 14 |- ( ( z = <. a , b >. /\ A _I a /\ BSingleton b ) <-> ( A _I a /\ BSingleton b /\ z = <. a , b >. ) )
21		vex 3203	. . . . . . . . . . . . . . . . 17 |- a e. _V
22	21	ideq 5274	. . . . . . . . . . . . . . . 16 |- ( A _I a <-> A = a )
23		eqcom 2629	. . . . . . . . . . . . . . . 16 |- ( A = a <-> a = A )
24	22, 23	bitri 264	. . . . . . . . . . . . . . 15 |- ( A _I a <-> a = A )
25		vex 3203	. . . . . . . . . . . . . . . 16 |- b e. _V
26	17, 25	brsingle 32024	. . . . . . . . . . . . . . 15 |- ( BSingleton b <-> b = { B } )
27		biid 251	. . . . . . . . . . . . . . 15 |- ( z = <. a , b >. <-> z = <. a , b >. )
28	24, 26, 27	3anbi123i 1251	. . . . . . . . . . . . . 14 |- ( ( A _I a /\ BSingleton b /\ z = <. a , b >. ) <-> ( a = A /\ b = { B } /\ z = <. a , b >. ) )
29	20, 28	bitri 264	. . . . . . . . . . . . 13 |- ( ( z = <. a , b >. /\ A _I a /\ BSingleton b ) <-> ( a = A /\ b = { B } /\ z = <. a , b >. ) )
30	29	2exbii 1775	. . . . . . . . . . . 12 |- ( E. a E. b ( z = <. a , b >. /\ A _I a /\ BSingleton b ) <-> E. a E. b ( a = A /\ b = { B } /\ z = <. a , b >. ) )
31		snex 4908	. . . . . . . . . . . . 13 |- { B } e. _V
32		opeq1 4402	. . . . . . . . . . . . . 14 |- ( a = A -> <. a , b >. = <. A , b >. )
33	32	eqeq2d 2632	. . . . . . . . . . . . 13 |- ( a = A -> ( z = <. a , b >. <-> z = <. A , b >. ) )
34		opeq2 4403	. . . . . . . . . . . . . 14 |- ( b = { B } -> <. A , b >. = <. A , { B } >. )
35	34	eqeq2d 2632	. . . . . . . . . . . . 13 |- ( b = { B } -> ( z = <. A , b >. <-> z = <. A , { B } >. ) )
36	16, 31, 33, 35	ceqsex2v 3245	. . . . . . . . . . . 12 |- ( E. a E. b ( a = A /\ b = { B } /\ z = <. a , b >. ) <-> z = <. A , { B } >. )
37	19, 30, 36	3bitri 286	. . . . . . . . . . 11 |- ( <. A , B >.pprod ( _I , Singleton ) z <-> z = <. A , { B } >. )
38	37	anbi1i 731	. . . . . . . . . 10 |- ( ( <. A , B >.pprod ( _I , Singleton ) z /\ z (Singleton o. Img ) y ) <-> ( z = <. A , { B } >. /\ z (Singleton o. Img ) y ) )
39	38	exbii 1774	. . . . . . . . 9 |- ( E. z ( <. A , B >.pprod ( _I , Singleton ) z /\ z (Singleton o. Img ) y ) <-> E. z ( z = <. A , { B } >. /\ z (Singleton o. Img ) y ) )
40		opex 4932	. . . . . . . . . . 11 |- <. A , { B } >. e. _V
41		breq1 4656	. . . . . . . . . . 11 |- ( z = <. A , { B } >. -> ( z (Singleton o. Img ) y <-> <. A , { B } >. (Singleton o. Img ) y ) )
42	40, 41	ceqsexv 3242	. . . . . . . . . 10 |- ( E. z ( z = <. A , { B } >. /\ z (Singleton o. Img ) y ) <-> <. A , { B } >. (Singleton o. Img ) y )
43	40, 14	brco 5292	. . . . . . . . . 10 |- ( <. A , { B } >. (Singleton o. Img ) y <-> E. x ( <. A , { B } >.Img x /\ xSingleton y ) )
44	16, 31, 12	brimg 32044	. . . . . . . . . . . . 13 |- ( <. A , { B } >.Img x <-> x = ( A " { B } ) )
45	12, 14	brsingle 32024	. . . . . . . . . . . . 13 |- ( xSingleton y <-> y = { x } )
46	44, 45	anbi12i 733	. . . . . . . . . . . 12 |- ( ( <. A , { B } >.Img x /\ xSingleton y ) <-> ( x = ( A " { B } ) /\ y = { x } ) )
47	46	exbii 1774	. . . . . . . . . . 11 |- ( E. x ( <. A , { B } >.Img x /\ xSingleton y ) <-> E. x ( x = ( A " { B } ) /\ y = { x } ) )
48		imaexg 7103	. . . . . . . . . . . . 13 |- ( A e. _V -> ( A " { B } ) e. _V )
49	16, 48	ax-mp 5	. . . . . . . . . . . 12 |- ( A " { B } ) e. _V
50		sneq 4187	. . . . . . . . . . . . 13 |- ( x = ( A " { B } ) -> { x } = { ( A " { B } ) } )
51	50	eqeq2d 2632	. . . . . . . . . . . 12 |- ( x = ( A " { B } ) -> ( y = { x } <-> y = { ( A " { B } ) } ) )
52	49, 51	ceqsexv 3242	. . . . . . . . . . 11 |- ( E. x ( x = ( A " { B } ) /\ y = { x } ) <-> y = { ( A " { B } ) } )
53	47, 52	bitri 264	. . . . . . . . . 10 |- ( E. x ( <. A , { B } >.Img x /\ xSingleton y ) <-> y = { ( A " { B } ) } )
54	42, 43, 53	3bitri 286	. . . . . . . . 9 |- ( E. z ( z = <. A , { B } >. /\ z (Singleton o. Img ) y ) <-> y = { ( A " { B } ) } )
55	15, 39, 54	3bitri 286	. . . . . . . 8 |- ( <. A , B >. ( (Singleton o. Img ) o. pprod ( _I , Singleton ) ) y <-> y = { ( A " { B } ) } )
56		eqid 2622	. . . . . . . . 9 |- ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) = ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) )
57		brxp 5147	. . . . . . . . . 10 |- ( y ( _V X. _V ) x <-> ( y e. _V /\ x e. _V ) )
58	14, 12, 57	mpbir2an 955	. . . . . . . . 9 |- y ( _V X. _V ) x
59		epel 5032	. . . . . . . . . . 11 |- ( z _E y <-> z e. y )
60	59	anbi1i 731	. . . . . . . . . 10 |- ( ( z _E y /\ z e. Singletons ) <-> ( z e. y /\ z e. Singletons ) )
61	14	brres 5402	. . . . . . . . . 10 |- ( z ( _E |` Singletons ) y <-> ( z _E y /\ z e. Singletons ) )
62		elin 3796	. . . . . . . . . 10 |- ( z e. ( y i^i Singletons ) <-> ( z e. y /\ z e. Singletons ) )
63	60, 61, 62	3bitr4ri 293	. . . . . . . . 9 |- ( z e. ( y i^i Singletons ) <-> z ( _E |` Singletons ) y )
64	14, 12, 56, 58, 63	brtxpsd3 32003	. . . . . . . 8 |- ( y ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) x <-> x = ( y i^i Singletons ) )
65	55, 64	anbi12i 733	. . . . . . 7 |- ( ( <. A , B >. ( (Singleton o. Img ) o. pprod ( _I , Singleton ) ) y /\ y ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) x ) <-> ( y = { ( A " { B } ) } /\ x = ( y i^i Singletons ) ) )
66	65	exbii 1774	. . . . . 6 |- ( E. y ( <. A , B >. ( (Singleton o. Img ) o. pprod ( _I , Singleton ) ) y /\ y ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) x ) <-> E. y ( y = { ( A " { B } ) } /\ x = ( y i^i Singletons ) ) )
67		ineq1 3807	. . . . . . . 8 |- ( y = { ( A " { B } ) } -> ( y i^i Singletons ) = ( { ( A " { B } ) } i^i Singletons ) )
68	67	eqeq2d 2632	. . . . . . 7 |- ( y = { ( A " { B } ) } -> ( x = ( y i^i Singletons ) <-> x = ( { ( A " { B } ) } i^i Singletons ) ) )
69	1, 68	ceqsexv 3242	. . . . . 6 |- ( E. y ( y = { ( A " { B } ) } /\ x = ( y i^i Singletons ) ) <-> x = ( { ( A " { B } ) } i^i Singletons ) )
70	13, 66, 69	3bitri 286	. . . . 5 |- ( <. A , B >. ( ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) o. ( (Singleton o. Img ) o. pprod ( _I , Singleton ) ) ) x <-> x = ( { ( A " { B } ) } i^i Singletons ) )
71	12, 10	brco 5292	. . . . . 6 |- ( x ( Bigcup o. Bigcup ) C <-> E. y ( x Bigcup y /\ y Bigcup C ) )
72	14	brbigcup 32005	. . . . . . . . 9 |- ( x Bigcup y <-> U. x = y )
73		eqcom 2629	. . . . . . . . 9 |- ( U. x = y <-> y = U. x )
74	72, 73	bitri 264	. . . . . . . 8 |- ( x Bigcup y <-> y = U. x )
75	10	brbigcup 32005	. . . . . . . . 9 |- ( y Bigcup C <-> U. y = C )
76		eqcom 2629	. . . . . . . . 9 |- ( U. y = C <-> C = U. y )
77	75, 76	bitri 264	. . . . . . . 8 |- ( y Bigcup C <-> C = U. y )
78	74, 77	anbi12i 733	. . . . . . 7 |- ( ( x Bigcup y /\ y Bigcup C ) <-> ( y = U. x /\ C = U. y ) )
79	78	exbii 1774	. . . . . 6 |- ( E. y ( x Bigcup y /\ y Bigcup C ) <-> E. y ( y = U. x /\ C = U. y ) )
80		vuniex 6954	. . . . . . 7 |- U. x e. _V
81		unieq 4444	. . . . . . . 8 |- ( y = U. x -> U. y = U. U. x )
82	81	eqeq2d 2632	. . . . . . 7 |- ( y = U. x -> ( C = U. y <-> C = U. U. x ) )
83	80, 82	ceqsexv 3242	. . . . . 6 |- ( E. y ( y = U. x /\ C = U. y ) <-> C = U. U. x )
84	71, 79, 83	3bitri 286	. . . . 5 |- ( x ( Bigcup o. Bigcup ) C <-> C = U. U. x )
85	70, 84	anbi12i 733	. . . 4 |- ( ( <. A , B >. ( ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) o. ( (Singleton o. Img ) o. pprod ( _I , Singleton ) ) ) x /\ x ( Bigcup o. Bigcup ) C ) <-> ( x = ( { ( A " { B } ) } i^i Singletons ) /\ C = U. U. x ) )
86	85	exbii 1774	. . 3 |- ( E. x ( <. A , B >. ( ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) o. ( (Singleton o. Img ) o. pprod ( _I , Singleton ) ) ) x /\ x ( Bigcup o. Bigcup ) C ) <-> E. x ( x = ( { ( A " { B } ) } i^i Singletons ) /\ C = U. U. x ) )
87	8, 11, 86	3bitri 286	. 2 |- ( <. A , B >.Apply C <-> E. x ( x = ( { ( A " { B } ) } i^i Singletons ) /\ C = U. U. x ) )
88		dffv5 32031	. . 3 |- ( A ` B ) = U. U. ( { ( A " { B } ) } i^i Singletons )
89	88	eqeq2i 2634	. 2 |- ( C = ( A ` B ) <-> C = U. U. ( { ( A " { B } ) } i^i Singletons ) )
90	6, 87, 89	3bitr4i 292	1 |- ( <. A , B >.Apply C <-> C = ( A ` B ) )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   _Vcvv 3200   \ cdif 3571   i^i cin 3573   /_\ csymdif 3843   {csn 4177   <.cop 4183   U.cuni 4436   class class class wbr 4653   _I cid 5023   _E cep 5028   X. cxp 5112   ran crn 5115   |` cres 5116   "cima 5117   o. ccom 5118   ` cfv 5888   (x) ctxp 31937  pprodcpprod 31938   Bigcupcbigcup 31941  Singletoncsingle 31945   Singletonscsingles 31946  Imgcimg 31949  Applycapply 31952

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-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-symdif 3844  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-eprel 5029  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-fo 5894  df-fv 5896  df-1st 7168  df-2nd 7169  df-txp 31961  df-pprod 31962  df-bigcup 31965  df-singleton 31969  df-singles 31970  df-image 31971  df-cart 31972  df-img 31973  df-apply 31980

This theorem is referenced by:  dfrecs2  32057  dfrdg4  32058