xpinpreima

Description: Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd , the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017)

		Ref	Expression
	Assertion	xpinpreima	⊢ ( 𝐴 × 𝐵 ) = ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ 𝐴 ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) “ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		inrab	⊢ ( { 𝑟 ∈ ( V × V ) ∣ ( 1^st ‘ 𝑟 ) ∈ 𝐴 } ∩ { 𝑟 ∈ ( V × V ) ∣ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 } ) = { 𝑟 ∈ ( V × V ) ∣ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) }
2		f1stres	⊢ ( 1^st ↾ ( V × V ) ) : ( V × V ) ⟶ V
3		ffn	⊢ ( ( 1^st ↾ ( V × V ) ) : ( V × V ) ⟶ V → ( 1^st ↾ ( V × V ) ) Fn ( V × V ) )
4		fncnvima2	⊢ ( ( 1^st ↾ ( V × V ) ) Fn ( V × V ) → ( ^◡ ( 1^st ↾ ( V × V ) ) “ 𝐴 ) = { 𝑟 ∈ ( V × V ) ∣ ( ( 1^st ↾ ( V × V ) ) ‘ 𝑟 ) ∈ 𝐴 } )
5	2 3 4	mp2b	⊢ ( ^◡ ( 1^st ↾ ( V × V ) ) “ 𝐴 ) = { 𝑟 ∈ ( V × V ) ∣ ( ( 1^st ↾ ( V × V ) ) ‘ 𝑟 ) ∈ 𝐴 }
6		fvres	⊢ ( 𝑟 ∈ ( V × V ) → ( ( 1^st ↾ ( V × V ) ) ‘ 𝑟 ) = ( 1^st ‘ 𝑟 ) )
7	6	eleq1d	⊢ ( 𝑟 ∈ ( V × V ) → ( ( ( 1^st ↾ ( V × V ) ) ‘ 𝑟 ) ∈ 𝐴 ↔ ( 1^st ‘ 𝑟 ) ∈ 𝐴 ) )
8	7	rabbiia	⊢ { 𝑟 ∈ ( V × V ) ∣ ( ( 1^st ↾ ( V × V ) ) ‘ 𝑟 ) ∈ 𝐴 } = { 𝑟 ∈ ( V × V ) ∣ ( 1^st ‘ 𝑟 ) ∈ 𝐴 }
9	5 8	eqtri	⊢ ( ^◡ ( 1^st ↾ ( V × V ) ) “ 𝐴 ) = { 𝑟 ∈ ( V × V ) ∣ ( 1^st ‘ 𝑟 ) ∈ 𝐴 }
10		f2ndres	⊢ ( 2^nd ↾ ( V × V ) ) : ( V × V ) ⟶ V
11		ffn	⊢ ( ( 2^nd ↾ ( V × V ) ) : ( V × V ) ⟶ V → ( 2^nd ↾ ( V × V ) ) Fn ( V × V ) )
12		fncnvima2	⊢ ( ( 2^nd ↾ ( V × V ) ) Fn ( V × V ) → ( ^◡ ( 2^nd ↾ ( V × V ) ) “ 𝐵 ) = { 𝑟 ∈ ( V × V ) ∣ ( ( 2^nd ↾ ( V × V ) ) ‘ 𝑟 ) ∈ 𝐵 } )
13	10 11 12	mp2b	⊢ ( ^◡ ( 2^nd ↾ ( V × V ) ) “ 𝐵 ) = { 𝑟 ∈ ( V × V ) ∣ ( ( 2^nd ↾ ( V × V ) ) ‘ 𝑟 ) ∈ 𝐵 }
14		fvres	⊢ ( 𝑟 ∈ ( V × V ) → ( ( 2^nd ↾ ( V × V ) ) ‘ 𝑟 ) = ( 2^nd ‘ 𝑟 ) )
15	14	eleq1d	⊢ ( 𝑟 ∈ ( V × V ) → ( ( ( 2^nd ↾ ( V × V ) ) ‘ 𝑟 ) ∈ 𝐵 ↔ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) )
16	15	rabbiia	⊢ { 𝑟 ∈ ( V × V ) ∣ ( ( 2^nd ↾ ( V × V ) ) ‘ 𝑟 ) ∈ 𝐵 } = { 𝑟 ∈ ( V × V ) ∣ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 }
17	13 16	eqtri	⊢ ( ^◡ ( 2^nd ↾ ( V × V ) ) “ 𝐵 ) = { 𝑟 ∈ ( V × V ) ∣ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 }
18	9 17	ineq12i	⊢ ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ 𝐴 ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) “ 𝐵 ) ) = ( { 𝑟 ∈ ( V × V ) ∣ ( 1^st ‘ 𝑟 ) ∈ 𝐴 } ∩ { 𝑟 ∈ ( V × V ) ∣ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 } )
19		xp2	⊢ ( 𝐴 × 𝐵 ) = { 𝑟 ∈ ( V × V ) ∣ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) }
20	1 18 19	3eqtr4ri	⊢ ( 𝐴 × 𝐵 ) = ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ 𝐴 ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) “ 𝐵 ) )

Metamath Proof Explorer

Theorem xpinpreima

Proof