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 ) )