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	⊢ 𝐴 ∈ V
	brimg.2	⊢ 𝐵 ∈ V
	brimg.3	⊢ 𝐶 ∈ V
Assertion	brimg	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ Img 𝐶 ↔ 𝐶 = ( 𝐴 “ 𝐵 ) )

Proof

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

Metamath Proof Explorer

Theorem brimg

Proof