Metamath Proof Explorer

Theorem brapply

Description: Binary relation form of the Apply function. (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Hypotheses brapply.1 
|- A e. _V
brapply.2 
|- B e. _V
brapply.3 
|- C e. _V
Assertion brapply 
|- ( <. A , B >. Apply C <-> C = ( A ` B ) )

Proof

Step Hyp Ref Expression
1 brapply.1 
 |-  A e. _V
2 brapply.2 
 |-  B e. _V
3 brapply.3 
 |-  C e. _V
4 snex 
 |-  { ( A " { B } ) } e. _V
5 4 inex1 
 |-  ( { ( A " { B } ) } i^i Singletons ) e. _V
6 unieq 
 |-  ( x = ( { ( A " { B } ) } i^i Singletons ) -> U. x = U. ( { ( A " { B } ) } i^i Singletons ) )
7 6 unieqd 
 |-  ( x = ( { ( A " { B } ) } i^i Singletons ) -> U. U. x = U. U. ( { ( A " { B } ) } i^i Singletons ) )
8 7 eqeq2d 
 |-  ( x = ( { ( A " { B } ) } i^i Singletons ) -> ( C = U. U. x <-> C = U. U. ( { ( A " { B } ) } i^i Singletons ) ) )
9 5 8 ceqsexv 
 |-  ( E. x ( x = ( { ( A " { B } ) } i^i Singletons ) /\ C = U. U. x ) <-> C = U. U. ( { ( A " { B } ) } i^i Singletons ) )
10 df-apply 
 |-  Apply = ( ( Bigcup o. Bigcup ) o. ( ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) o. ( ( Singleton o. Img ) o. pprod ( _I , Singleton ) ) ) )
11 10 breqi 
 |-  ( <. 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 )
12 opex 
 |-  <. A , B >. e. _V
13 12 3 brco 
 |-  ( <. 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 ) )
14 vex 
 |-  x e. _V
15 12 14 brco 
 |-  ( <. 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 ) )
16 vex 
 |-  y e. _V
17 12 16 brco 
 |-  ( <. A , B >. ( ( Singleton o. Img ) o. pprod ( _I , Singleton ) ) y <-> E. z ( <. A , B >. pprod ( _I , Singleton ) z /\ z ( Singleton o. Img ) y ) )
18 vex 
 |-  z e. _V
19 1 2 18 brpprod3a 
 |-  ( <. A , B >. pprod ( _I , Singleton ) z <-> E. a E. b ( z = <. a , b >. /\ A _I a /\ B Singleton b ) )
20 3anrot 
 |-  ( ( z = <. a , b >. /\ A _I a /\ B Singleton b ) <-> ( A _I a /\ B Singleton b /\ z = <. a , b >. ) )
21 vex 
 |-  a e. _V
22 21 ideq 
 |-  ( A _I a <-> A = a )
23 eqcom 
 |-  ( A = a <-> a = A )
24 22 23 bitri 
 |-  ( A _I a <-> a = A )
25 vex 
 |-  b e. _V
26 2 25 brsingle 
 |-  ( B Singleton b <-> b = { B } )
27 biid 
 |-  ( z = <. a , b >. <-> z = <. a , b >. )
28 24 26 27 3anbi123i 
 |-  ( ( A _I a /\ B Singleton b /\ z = <. a , b >. ) <-> ( a = A /\ b = { B } /\ z = <. a , b >. ) )
29 20 28 bitri 
 |-  ( ( z = <. a , b >. /\ A _I a /\ B Singleton b ) <-> ( a = A /\ b = { B } /\ z = <. a , b >. ) )
30 29 2exbii 
 |-  ( E. a E. b ( z = <. a , b >. /\ A _I a /\ B Singleton b ) <-> E. a E. b ( a = A /\ b = { B } /\ z = <. a , b >. ) )
31 snex 
 |-  { B } e. _V
32 opeq1 
 |-  ( a = A -> <. a , b >. = <. A , b >. )
33 32 eqeq2d 
 |-  ( a = A -> ( z = <. a , b >. <-> z = <. A , b >. ) )
34 opeq2 
 |-  ( b = { B } -> <. A , b >. = <. A , { B } >. )
35 34 eqeq2d 
 |-  ( b = { B } -> ( z = <. A , b >. <-> z = <. A , { B } >. ) )
36 1 31 33 35 ceqsex2v 
 |-  ( E. a E. b ( a = A /\ b = { B } /\ z = <. a , b >. ) <-> z = <. A , { B } >. )
37 19 30 36 3bitri 
 |-  ( <. A , B >. pprod ( _I , Singleton ) z <-> z = <. A , { B } >. )
38 37 anbi1i 
 |-  ( ( <. A , B >. pprod ( _I , Singleton ) z /\ z ( Singleton o. Img ) y ) <-> ( z = <. A , { B } >. /\ z ( Singleton o. Img ) y ) )
39 38 exbii 
 |-  ( 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 
 |-  <. A , { B } >. e. _V
41 breq1 
 |-  ( z = <. A , { B } >. -> ( z ( Singleton o. Img ) y <-> <. A , { B } >. ( Singleton o. Img ) y ) )
42 40 41 ceqsexv 
 |-  ( E. z ( z = <. A , { B } >. /\ z ( Singleton o. Img ) y ) <-> <. A , { B } >. ( Singleton o. Img ) y )
43 40 16 brco 
 |-  ( <. A , { B } >. ( Singleton o. Img ) y <-> E. x ( <. A , { B } >. Img x /\ x Singleton y ) )
44 1 31 14 brimg 
 |-  ( <. A , { B } >. Img x <-> x = ( A " { B } ) )
45 14 16 brsingle 
 |-  ( x Singleton y <-> y = { x } )
46 44 45 anbi12i 
 |-  ( ( <. A , { B } >. Img x /\ x Singleton y ) <-> ( x = ( A " { B } ) /\ y = { x } ) )
47 46 exbii 
 |-  ( E. x ( <. A , { B } >. Img x /\ x Singleton y ) <-> E. x ( x = ( A " { B } ) /\ y = { x } ) )
48 1 imaex 
 |-  ( A " { B } ) e. _V
49 sneq 
 |-  ( x = ( A " { B } ) -> { x } = { ( A " { B } ) } )
50 49 eqeq2d 
 |-  ( x = ( A " { B } ) -> ( y = { x } <-> y = { ( A " { B } ) } ) )
51 48 50 ceqsexv 
 |-  ( E. x ( x = ( A " { B } ) /\ y = { x } ) <-> y = { ( A " { B } ) } )
52 47 51 bitri 
 |-  ( E. x ( <. A , { B } >. Img x /\ x Singleton y ) <-> y = { ( A " { B } ) } )
53 42 43 52 3bitri 
 |-  ( E. z ( z = <. A , { B } >. /\ z ( Singleton o. Img ) y ) <-> y = { ( A " { B } ) } )
54 17 39 53 3bitri 
 |-  ( <. A , B >. ( ( Singleton o. Img ) o. pprod ( _I , Singleton ) ) y <-> y = { ( A " { B } ) } )
55 eqid 
 |-  ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) = ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) )
56 brxp 
 |-  ( y ( _V X. _V ) x <-> ( y e. _V /\ x e. _V ) )
57 16 14 56 mpbir2an 
 |-  y ( _V X. _V ) x
58 epel 
 |-  ( z _E y <-> z e. y )
59 58 anbi1ci 
 |-  ( ( z e. Singletons /\ z _E y ) <-> ( z e. y /\ z e. Singletons ) )
60 16 brresi 
 |-  ( z ( _E |` Singletons ) y <-> ( z e. Singletons /\ z _E y ) )
61 elin 
 |-  ( z e. ( y i^i Singletons ) <-> ( z e. y /\ z e. Singletons ) )
62 59 60 61 3bitr4ri 
 |-  ( z e. ( y i^i Singletons ) <-> z ( _E |` Singletons ) y )
63 16 14 55 57 62 brtxpsd3 
 |-  ( y ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) x <-> x = ( y i^i Singletons ) )
64 54 63 anbi12i 
 |-  ( ( <. 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 ) ) )
65 64 exbii 
 |-  ( 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 ) ) )
66 ineq1 
 |-  ( y = { ( A " { B } ) } -> ( y i^i Singletons ) = ( { ( A " { B } ) } i^i Singletons ) )
67 66 eqeq2d 
 |-  ( y = { ( A " { B } ) } -> ( x = ( y i^i Singletons ) <-> x = ( { ( A " { B } ) } i^i Singletons ) ) )
68 4 67 ceqsexv 
 |-  ( E. y ( y = { ( A " { B } ) } /\ x = ( y i^i Singletons ) ) <-> x = ( { ( A " { B } ) } i^i Singletons ) )
69 15 65 68 3bitri 
 |-  ( <. 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 ) )
70 14 3 brco 
 |-  ( x ( Bigcup o. Bigcup ) C <-> E. y ( x Bigcup y /\ y Bigcup C ) )
71 16 brbigcup 
 |-  ( x Bigcup y <-> U. x = y )
72 eqcom 
 |-  ( U. x = y <-> y = U. x )
73 71 72 bitri 
 |-  ( x Bigcup y <-> y = U. x )
74 3 brbigcup 
 |-  ( y Bigcup C <-> U. y = C )
75 eqcom 
 |-  ( U. y = C <-> C = U. y )
76 74 75 bitri 
 |-  ( y Bigcup C <-> C = U. y )
77 73 76 anbi12i 
 |-  ( ( x Bigcup y /\ y Bigcup C ) <-> ( y = U. x /\ C = U. y ) )
78 77 exbii 
 |-  ( E. y ( x Bigcup y /\ y Bigcup C ) <-> E. y ( y = U. x /\ C = U. y ) )
79 vuniex 
 |-  U. x e. _V
80 unieq 
 |-  ( y = U. x -> U. y = U. U. x )
81 80 eqeq2d 
 |-  ( y = U. x -> ( C = U. y <-> C = U. U. x ) )
82 79 81 ceqsexv 
 |-  ( E. y ( y = U. x /\ C = U. y ) <-> C = U. U. x )
83 70 78 82 3bitri 
 |-  ( x ( Bigcup o. Bigcup ) C <-> C = U. U. x )
84 69 83 anbi12i 
 |-  ( ( <. 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 ) )
85 84 exbii 
 |-  ( 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 ) )
86 11 13 85 3bitri 
 |-  ( <. A , B >. Apply C <-> E. x ( x = ( { ( A " { B } ) } i^i Singletons ) /\ C = U. U. x ) )
87 dffv5 
 |-  ( A ` B ) = U. U. ( { ( A " { B } ) } i^i Singletons )
88 87 eqeq2i 
 |-  ( C = ( A ` B ) <-> C = U. U. ( { ( A " { B } ) } i^i Singletons ) )
89 9 86 88 3bitr4i 
 |-  ( <. A , B >. Apply C <-> C = ( A ` B ) )