xpinpreima2

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	xpinpreima2	⊢ ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) → ( 𝐴 × 𝐵 ) = ( ( ^◡ ( 1^st ↾ ( 𝐸 × 𝐹 ) ) “ 𝐴 ) ∩ ( ^◡ ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) “ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xp2	⊢ ( 𝐴 × 𝐵 ) = { 𝑟 ∈ ( V × V ) ∣ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) }
2		xpss	⊢ ( 𝐸 × 𝐹 ) ⊆ ( V × V )
3		rabss2	⊢ ( ( 𝐸 × 𝐹 ) ⊆ ( V × V ) → { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) } ⊆ { 𝑟 ∈ ( V × V ) ∣ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) } )
4	2 3	mp1i	⊢ ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) → { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) } ⊆ { 𝑟 ∈ ( V × V ) ∣ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) } )
5		simprl	⊢ ( ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) ∧ ( 𝑟 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) ) ) → 𝑟 ∈ ( V × V ) )
6		simpll	⊢ ( ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) ∧ ( 𝑟 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) ) ) → 𝐴 ⊆ 𝐸 )
7		simprrl	⊢ ( ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) ∧ ( 𝑟 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) ) ) → ( 1^st ‘ 𝑟 ) ∈ 𝐴 )
8	6 7	sseldd	⊢ ( ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) ∧ ( 𝑟 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) ) ) → ( 1^st ‘ 𝑟 ) ∈ 𝐸 )
9		simplr	⊢ ( ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) ∧ ( 𝑟 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) ) ) → 𝐵 ⊆ 𝐹 )
10		simprrr	⊢ ( ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) ∧ ( 𝑟 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) ) ) → ( 2^nd ‘ 𝑟 ) ∈ 𝐵 )
11	9 10	sseldd	⊢ ( ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) ∧ ( 𝑟 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) ) ) → ( 2^nd ‘ 𝑟 ) ∈ 𝐹 )
12	8 11	jca	⊢ ( ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) ∧ ( 𝑟 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) ) ) → ( ( 1^st ‘ 𝑟 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐹 ) )
13		elxp7	⊢ ( 𝑟 ∈ ( 𝐸 × 𝐹 ) ↔ ( 𝑟 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑟 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐹 ) ) )
14	5 12 13	sylanbrc	⊢ ( ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) ∧ ( 𝑟 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) ) ) → 𝑟 ∈ ( 𝐸 × 𝐹 ) )
15	14	rabss3d	⊢ ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) → { 𝑟 ∈ ( V × V ) ∣ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) } ⊆ { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) } )
16	4 15	eqssd	⊢ ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) → { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) } = { 𝑟 ∈ ( V × V ) ∣ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) } )
17	1 16	eqtr4id	⊢ ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) → ( 𝐴 × 𝐵 ) = { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) } )
18		inrab	⊢ ( { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( 1^st ‘ 𝑟 ) ∈ 𝐴 } ∩ { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 } ) = { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( ( 1^st ‘ 𝑟 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) }
19	17 18	eqtr4di	⊢ ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) → ( 𝐴 × 𝐵 ) = ( { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( 1^st ‘ 𝑟 ) ∈ 𝐴 } ∩ { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 } ) )
20		f1stres	⊢ ( 1^st ↾ ( 𝐸 × 𝐹 ) ) : ( 𝐸 × 𝐹 ) ⟶ 𝐸
21		ffn	⊢ ( ( 1^st ↾ ( 𝐸 × 𝐹 ) ) : ( 𝐸 × 𝐹 ) ⟶ 𝐸 → ( 1^st ↾ ( 𝐸 × 𝐹 ) ) Fn ( 𝐸 × 𝐹 ) )
22		fncnvima2	⊢ ( ( 1^st ↾ ( 𝐸 × 𝐹 ) ) Fn ( 𝐸 × 𝐹 ) → ( ^◡ ( 1^st ↾ ( 𝐸 × 𝐹 ) ) “ 𝐴 ) = { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( ( 1^st ↾ ( 𝐸 × 𝐹 ) ) ‘ 𝑟 ) ∈ 𝐴 } )
23	20 21 22	mp2b	⊢ ( ^◡ ( 1^st ↾ ( 𝐸 × 𝐹 ) ) “ 𝐴 ) = { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( ( 1^st ↾ ( 𝐸 × 𝐹 ) ) ‘ 𝑟 ) ∈ 𝐴 }
24		fvres	⊢ ( 𝑟 ∈ ( 𝐸 × 𝐹 ) → ( ( 1^st ↾ ( 𝐸 × 𝐹 ) ) ‘ 𝑟 ) = ( 1^st ‘ 𝑟 ) )
25	24	eleq1d	⊢ ( 𝑟 ∈ ( 𝐸 × 𝐹 ) → ( ( ( 1^st ↾ ( 𝐸 × 𝐹 ) ) ‘ 𝑟 ) ∈ 𝐴 ↔ ( 1^st ‘ 𝑟 ) ∈ 𝐴 ) )
26	25	rabbiia	⊢ { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( ( 1^st ↾ ( 𝐸 × 𝐹 ) ) ‘ 𝑟 ) ∈ 𝐴 } = { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( 1^st ‘ 𝑟 ) ∈ 𝐴 }
27	23 26	eqtri	⊢ ( ^◡ ( 1^st ↾ ( 𝐸 × 𝐹 ) ) “ 𝐴 ) = { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( 1^st ‘ 𝑟 ) ∈ 𝐴 }
28		f2ndres	⊢ ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) : ( 𝐸 × 𝐹 ) ⟶ 𝐹
29		ffn	⊢ ( ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) : ( 𝐸 × 𝐹 ) ⟶ 𝐹 → ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) Fn ( 𝐸 × 𝐹 ) )
30		fncnvima2	⊢ ( ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) Fn ( 𝐸 × 𝐹 ) → ( ^◡ ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) “ 𝐵 ) = { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) ‘ 𝑟 ) ∈ 𝐵 } )
31	28 29 30	mp2b	⊢ ( ^◡ ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) “ 𝐵 ) = { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) ‘ 𝑟 ) ∈ 𝐵 }
32		fvres	⊢ ( 𝑟 ∈ ( 𝐸 × 𝐹 ) → ( ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) ‘ 𝑟 ) = ( 2^nd ‘ 𝑟 ) )
33	32	eleq1d	⊢ ( 𝑟 ∈ ( 𝐸 × 𝐹 ) → ( ( ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) ‘ 𝑟 ) ∈ 𝐵 ↔ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 ) )
34	33	rabbiia	⊢ { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) ‘ 𝑟 ) ∈ 𝐵 } = { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 }
35	31 34	eqtri	⊢ ( ^◡ ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) “ 𝐵 ) = { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 }
36	27 35	ineq12i	⊢ ( ( ^◡ ( 1^st ↾ ( 𝐸 × 𝐹 ) ) “ 𝐴 ) ∩ ( ^◡ ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) “ 𝐵 ) ) = ( { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( 1^st ‘ 𝑟 ) ∈ 𝐴 } ∩ { 𝑟 ∈ ( 𝐸 × 𝐹 ) ∣ ( 2^nd ‘ 𝑟 ) ∈ 𝐵 } )
37	19 36	eqtr4di	⊢ ( ( 𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹 ) → ( 𝐴 × 𝐵 ) = ( ( ^◡ ( 1^st ↾ ( 𝐸 × 𝐹 ) ) “ 𝐴 ) ∩ ( ^◡ ( 2^nd ↾ ( 𝐸 × 𝐹 ) ) “ 𝐵 ) ) )

Metamath Proof Explorer

Theorem xpinpreima2

Proof