This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brimg

Description: Binary relation form of the Img 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 brimg.1 
|- A e. _V
brimg.2 
|- B e. _V
brimg.3 
|- C e. _V
Assertion brimg 
|- ( <. A , B >. Img C <-> C = ( A " B ) )

Proof

Step Hyp Ref Expression
1 brimg.1 
 |-  A e. _V
2 brimg.2 
 |-  B e. _V
3 brimg.3 
 |-  C e. _V
4 df-img 
 |-  Img = ( Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) o. Cart )
5 4 breqi 
 |-  ( <. A , B >. Img C <-> <. A , B >. ( Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) o. Cart ) C )
6 opex 
 |-  <. A , B >. e. _V
7 6 3 brco 
 |-  ( <. A , B >. ( Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) o. Cart ) C <-> E. a ( <. A , B >. Cart a /\ a Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) C ) )
8 vex 
 |-  a e. _V
9 1 2 8 brcart 
 |-  ( <. A , B >. Cart a <-> a = ( A X. B ) )
10 9 anbi1i 
 |-  ( ( <. A , B >. Cart a /\ a Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) C ) <-> ( a = ( A X. B ) /\ a Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) C ) )
11 10 exbii 
 |-  ( E. a ( <. A , B >. Cart a /\ a Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) C ) <-> E. a ( a = ( A X. B ) /\ a Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) C ) )
12 1 2 xpex 
 |-  ( A X. B ) e. _V
13 breq1 
 |-  ( a = ( A X. B ) -> ( a Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) C <-> ( A X. B ) Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) C ) )
14 12 13 ceqsexv 
 |-  ( E. a ( a = ( A X. B ) /\ a Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) C ) <-> ( A X. B ) Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) C )
15 7 11 14 3bitri 
 |-  ( <. A , B >. ( Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) o. Cart ) C <-> ( A X. B ) Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) C )
16 12 3 brimage 
 |-  ( ( A X. B ) Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) C <-> C = ( ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) " ( A X. B ) ) )
17 19.42v 
 |-  ( E. a ( b e. B /\ ( a e. A /\ <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) <-> ( b e. B /\ E. a ( a e. A /\ <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) )
18 anass 
 |-  ( ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) <-> ( p = <. a , b >. /\ ( ( a e. A /\ b e. B ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) )
19 an21 
 |-  ( ( ( a e. A /\ b e. B ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) <-> ( b e. B /\ ( a e. A /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) )
20 19 anbi2i 
 |-  ( ( p = <. a , b >. /\ ( ( a e. A /\ b e. B ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) <-> ( p = <. a , b >. /\ ( b e. B /\ ( a e. A /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) ) )
21 18 20 bitri 
 |-  ( ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) <-> ( p = <. a , b >. /\ ( b e. B /\ ( a e. A /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) ) )
22 21 2exbii 
 |-  ( E. p E. a ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) <-> E. p E. a ( p = <. a , b >. /\ ( b e. B /\ ( a e. A /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) ) )
23 excom 
 |-  ( E. p E. a ( p = <. a , b >. /\ ( b e. B /\ ( a e. A /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) ) <-> E. a E. p ( p = <. a , b >. /\ ( b e. B /\ ( a e. A /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) ) )
24 opex 
 |-  <. a , b >. e. _V
25 breq1 
 |-  ( p = <. a , b >. -> ( p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x <-> <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) )
26 25 anbi2d 
 |-  ( p = <. a , b >. -> ( ( a e. A /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) <-> ( a e. A /\ <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) )
27 26 anbi2d 
 |-  ( p = <. a , b >. -> ( ( b e. B /\ ( a e. A /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) <-> ( b e. B /\ ( a e. A /\ <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) ) )
28 24 27 ceqsexv 
 |-  ( E. p ( p = <. a , b >. /\ ( b e. B /\ ( a e. A /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) ) <-> ( b e. B /\ ( a e. A /\ <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) )
29 28 exbii 
 |-  ( E. a E. p ( p = <. a , b >. /\ ( b e. B /\ ( a e. A /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) ) <-> E. a ( b e. B /\ ( a e. A /\ <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) )
30 22 23 29 3bitri 
 |-  ( E. p E. a ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) <-> E. a ( b e. B /\ ( a e. A /\ <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) )
31 df-br 
 |-  ( b A x <-> <. b , x >. e. A )
32 risset 
 |-  ( <. b , x >. e. A <-> E. a e. A a = <. b , x >. )
33 vex 
 |-  b e. _V
34 33 brresi 
 |-  ( a ( 1st |` ( _V X. _V ) ) b <-> ( a e. ( _V X. _V ) /\ a 1st b ) )
35 df-br 
 |-  ( a ( 1st |` ( _V X. _V ) ) b <-> <. a , b >. e. ( 1st |` ( _V X. _V ) ) )
36 34 35 bitr3i 
 |-  ( ( a e. ( _V X. _V ) /\ a 1st b ) <-> <. a , b >. e. ( 1st |` ( _V X. _V ) ) )
37 36 anbi1i 
 |-  ( ( ( a e. ( _V X. _V ) /\ a 1st b ) /\ <. a , b >. ( 2nd o. 1st ) x ) <-> ( <. a , b >. e. ( 1st |` ( _V X. _V ) ) /\ <. a , b >. ( 2nd o. 1st ) x ) )
38 elvv 
 |-  ( a e. ( _V X. _V ) <-> E. p E. q a = <. p , q >. )
39 38 anbi1i 
 |-  ( ( a e. ( _V X. _V ) /\ ( a 1st b /\ <. a , b >. ( 2nd o. 1st ) x ) ) <-> ( E. p E. q a = <. p , q >. /\ ( a 1st b /\ <. a , b >. ( 2nd o. 1st ) x ) ) )
40 anass 
 |-  ( ( ( a e. ( _V X. _V ) /\ a 1st b ) /\ <. a , b >. ( 2nd o. 1st ) x ) <-> ( a e. ( _V X. _V ) /\ ( a 1st b /\ <. a , b >. ( 2nd o. 1st ) x ) ) )
41 ancom 
 |-  ( ( a = <. p , q >. /\ ( p = b /\ q = x ) ) <-> ( ( p = b /\ q = x ) /\ a = <. p , q >. ) )
42 breq1 
 |-  ( a = <. p , q >. -> ( a 1st b <-> <. p , q >. 1st b ) )
43 opeq1 
 |-  ( a = <. p , q >. -> <. a , b >. = <. <. p , q >. , b >. )
44 43 breq1d 
 |-  ( a = <. p , q >. -> ( <. a , b >. ( 2nd o. 1st ) x <-> <. <. p , q >. , b >. ( 2nd o. 1st ) x ) )
45 42 44 anbi12d 
 |-  ( a = <. p , q >. -> ( ( a 1st b /\ <. a , b >. ( 2nd o. 1st ) x ) <-> ( <. p , q >. 1st b /\ <. <. p , q >. , b >. ( 2nd o. 1st ) x ) ) )
46 vex 
 |-  p e. _V
47 vex 
 |-  q e. _V
48 46 47 br1steq 
 |-  ( <. p , q >. 1st b <-> b = p )
49 equcom 
 |-  ( b = p <-> p = b )
50 48 49 bitri 
 |-  ( <. p , q >. 1st b <-> p = b )
51 opex 
 |-  <. <. p , q >. , b >. e. _V
52 vex 
 |-  x e. _V
53 51 52 brco 
 |-  ( <. <. p , q >. , b >. ( 2nd o. 1st ) x <-> E. a ( <. <. p , q >. , b >. 1st a /\ a 2nd x ) )
54 opex 
 |-  <. p , q >. e. _V
55 54 33 br1steq 
 |-  ( <. <. p , q >. , b >. 1st a <-> a = <. p , q >. )
56 55 anbi1i 
 |-  ( ( <. <. p , q >. , b >. 1st a /\ a 2nd x ) <-> ( a = <. p , q >. /\ a 2nd x ) )
57 56 exbii 
 |-  ( E. a ( <. <. p , q >. , b >. 1st a /\ a 2nd x ) <-> E. a ( a = <. p , q >. /\ a 2nd x ) )
58 53 57 bitri 
 |-  ( <. <. p , q >. , b >. ( 2nd o. 1st ) x <-> E. a ( a = <. p , q >. /\ a 2nd x ) )
59 breq1 
 |-  ( a = <. p , q >. -> ( a 2nd x <-> <. p , q >. 2nd x ) )
60 54 59 ceqsexv 
 |-  ( E. a ( a = <. p , q >. /\ a 2nd x ) <-> <. p , q >. 2nd x )
61 46 47 br2ndeq 
 |-  ( <. p , q >. 2nd x <-> x = q )
62 60 61 bitri 
 |-  ( E. a ( a = <. p , q >. /\ a 2nd x ) <-> x = q )
63 equcom 
 |-  ( x = q <-> q = x )
64 58 62 63 3bitri 
 |-  ( <. <. p , q >. , b >. ( 2nd o. 1st ) x <-> q = x )
65 50 64 anbi12i 
 |-  ( ( <. p , q >. 1st b /\ <. <. p , q >. , b >. ( 2nd o. 1st ) x ) <-> ( p = b /\ q = x ) )
66 45 65 bitrdi 
 |-  ( a = <. p , q >. -> ( ( a 1st b /\ <. a , b >. ( 2nd o. 1st ) x ) <-> ( p = b /\ q = x ) ) )
67 66 pm5.32i 
 |-  ( ( a = <. p , q >. /\ ( a 1st b /\ <. a , b >. ( 2nd o. 1st ) x ) ) <-> ( a = <. p , q >. /\ ( p = b /\ q = x ) ) )
68 df-3an 
 |-  ( ( p = b /\ q = x /\ a = <. p , q >. ) <-> ( ( p = b /\ q = x ) /\ a = <. p , q >. ) )
69 41 67 68 3bitr4i 
 |-  ( ( a = <. p , q >. /\ ( a 1st b /\ <. a , b >. ( 2nd o. 1st ) x ) ) <-> ( p = b /\ q = x /\ a = <. p , q >. ) )
70 69 2exbii 
 |-  ( E. p E. q ( a = <. p , q >. /\ ( a 1st b /\ <. a , b >. ( 2nd o. 1st ) x ) ) <-> E. p E. q ( p = b /\ q = x /\ a = <. p , q >. ) )
71 19.41vv 
 |-  ( E. p E. q ( a = <. p , q >. /\ ( a 1st b /\ <. a , b >. ( 2nd o. 1st ) x ) ) <-> ( E. p E. q a = <. p , q >. /\ ( a 1st b /\ <. a , b >. ( 2nd o. 1st ) x ) ) )
72 opeq1 
 |-  ( p = b -> <. p , q >. = <. b , q >. )
73 72 eqeq2d 
 |-  ( p = b -> ( a = <. p , q >. <-> a = <. b , q >. ) )
74 opeq2 
 |-  ( q = x -> <. b , q >. = <. b , x >. )
75 74 eqeq2d 
 |-  ( q = x -> ( a = <. b , q >. <-> a = <. b , x >. ) )
76 33 52 73 75 ceqsex2v 
 |-  ( E. p E. q ( p = b /\ q = x /\ a = <. p , q >. ) <-> a = <. b , x >. )
77 70 71 76 3bitr3ri 
 |-  ( a = <. b , x >. <-> ( E. p E. q a = <. p , q >. /\ ( a 1st b /\ <. a , b >. ( 2nd o. 1st ) x ) ) )
78 39 40 77 3bitr4ri 
 |-  ( a = <. b , x >. <-> ( ( a e. ( _V X. _V ) /\ a 1st b ) /\ <. a , b >. ( 2nd o. 1st ) x ) )
79 52 brresi 
 |-  ( <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x <-> ( <. a , b >. e. ( 1st |` ( _V X. _V ) ) /\ <. a , b >. ( 2nd o. 1st ) x ) )
80 37 78 79 3bitr4i 
 |-  ( a = <. b , x >. <-> <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x )
81 80 rexbii 
 |-  ( E. a e. A a = <. b , x >. <-> E. a e. A <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x )
82 32 81 bitri 
 |-  ( <. b , x >. e. A <-> E. a e. A <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x )
83 df-rex 
 |-  ( E. a e. A <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x <-> E. a ( a e. A /\ <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) )
84 31 82 83 3bitri 
 |-  ( b A x <-> E. a ( a e. A /\ <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) )
85 84 anbi2i 
 |-  ( ( b e. B /\ b A x ) <-> ( b e. B /\ E. a ( a e. A /\ <. a , b >. ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) ) )
86 17 30 85 3bitr4ri 
 |-  ( ( b e. B /\ b A x ) <-> E. p E. a ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) )
87 86 exbii 
 |-  ( E. b ( b e. B /\ b A x ) <-> E. b E. p E. a ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) )
88 52 elima2 
 |-  ( x e. ( A " B ) <-> E. b ( b e. B /\ b A x ) )
89 52 elima2 
 |-  ( x e. ( ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) " ( A X. B ) ) <-> E. p ( p e. ( A X. B ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) )
90 elxp 
 |-  ( p e. ( A X. B ) <-> E. a E. b ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) )
91 90 anbi1i 
 |-  ( ( p e. ( A X. B ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) <-> ( E. a E. b ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) )
92 19.41vv 
 |-  ( E. a E. b ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) <-> ( E. a E. b ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) )
93 91 92 bitr4i 
 |-  ( ( p e. ( A X. B ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) <-> E. a E. b ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) )
94 93 exbii 
 |-  ( E. p ( p e. ( A X. B ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) <-> E. p E. a E. b ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) )
95 exrot3 
 |-  ( E. p E. a E. b ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) <-> E. a E. b E. p ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) )
96 exrot3 
 |-  ( E. a E. b E. p ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) <-> E. b E. p E. a ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) )
97 95 96 bitri 
 |-  ( E. p E. a E. b ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) <-> E. b E. p E. a ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) )
98 89 94 97 3bitri 
 |-  ( x e. ( ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) " ( A X. B ) ) <-> E. b E. p E. a ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ p ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) x ) )
99 87 88 98 3bitr4ri 
 |-  ( x e. ( ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) " ( A X. B ) ) <-> x e. ( A " B ) )
100 99 eqriv 
 |-  ( ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) " ( A X. B ) ) = ( A " B )
101 100 eqeq2i 
 |-  ( C = ( ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) " ( A X. B ) ) <-> C = ( A " B ) )
102 16 101 bitri 
 |-  ( ( A X. B ) Image ( ( 2nd o. 1st ) |` ( 1st |` ( _V X. _V ) ) ) C <-> C = ( A " B ) )
103 5 15 102 3bitri 
 |-  ( <. A , B >. Img C <-> C = ( A " B ) )