Metamath Proof Explorer

Theorem df1stres

Description: Definition for a restriction of the 1st (first member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017)

		Ref	Expression
	Assertion	df1stres	⊢ ( 1^st ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		df1st2	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } = ( 1^st ↾ ( V × V ) )
2	1	reseq1i	⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ↾ ( 𝐴 × 𝐵 ) ) = ( ( 1^st ↾ ( V × V ) ) ↾ ( 𝐴 × 𝐵 ) )
3		resoprab	⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ↾ ( 𝐴 × 𝐵 ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝑥 ) }
4		resres	⊢ ( ( 1^st ↾ ( V × V ) ) ↾ ( 𝐴 × 𝐵 ) ) = ( 1^st ↾ ( ( V × V ) ∩ ( 𝐴 × 𝐵 ) ) )
5		incom	⊢ ( ( 𝐴 × 𝐵 ) ∩ ( V × V ) ) = ( ( V × V ) ∩ ( 𝐴 × 𝐵 ) )
6		xpss	⊢ ( 𝐴 × 𝐵 ) ⊆ ( V × V )
7		dfss2	⊢ ( ( 𝐴 × 𝐵 ) ⊆ ( V × V ) ↔ ( ( 𝐴 × 𝐵 ) ∩ ( V × V ) ) = ( 𝐴 × 𝐵 ) )
8	6 7	mpbi	⊢ ( ( 𝐴 × 𝐵 ) ∩ ( V × V ) ) = ( 𝐴 × 𝐵 )
9	5 8	eqtr3i	⊢ ( ( V × V ) ∩ ( 𝐴 × 𝐵 ) ) = ( 𝐴 × 𝐵 )
10	9	reseq2i	⊢ ( 1^st ↾ ( ( V × V ) ∩ ( 𝐴 × 𝐵 ) ) ) = ( 1^st ↾ ( 𝐴 × 𝐵 ) )
11	4 10	eqtri	⊢ ( ( 1^st ↾ ( V × V ) ) ↾ ( 𝐴 × 𝐵 ) ) = ( 1^st ↾ ( 𝐴 × 𝐵 ) )
12	2 3 11	3eqtr3ri	⊢ ( 1^st ↾ ( 𝐴 × 𝐵 ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝑥 ) }
13		df-mpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑥 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝑥 ) }
14	12 13	eqtr4i	⊢ ( 1^st ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑥 )