Theorem f1stres

Description: Mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 11-Oct-2004) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	f1stres	⊢ ( 1st ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐴

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑦 ∈ V
2		vex	⊢ 𝑧 ∈ V
3	1 2	op1sta	⊢ ∪ dom { ⟨ 𝑦 , 𝑧 ⟩ } = 𝑦
4	3	eleq1i	⊢ ( ∪ dom { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 )
5	4	biranri	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ∪ dom { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐴 )
6	5	rgen2	⊢ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∪ dom { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐴
7		sneq	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → { 𝑥 } = { ⟨ 𝑦 , 𝑧 ⟩ } )
8	7	dmeqd	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → dom { 𝑥 } = dom { ⟨ 𝑦 , 𝑧 ⟩ } )
9	8	unieqd	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ∪ dom { 𝑥 } = ∪ dom { ⟨ 𝑦 , 𝑧 ⟩ } )
10	9	eleq1d	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ∪ dom { 𝑥 } ∈ 𝐴 ↔ ∪ dom { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐴 ) )
11	10	ralxp	⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ dom { 𝑥 } ∈ 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∪ dom { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐴 )
12	6 11	mpbir	⊢ ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ dom { 𝑥 } ∈ 𝐴
13		df-1st	⊢ 1st = ( 𝑥 ∈ V ↦ ∪ dom { 𝑥 } )
14	13	reseq1i	⊢ ( 1st ↾ ( 𝐴 × 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ ∪ dom { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) )
15		ssv	⊢ ( 𝐴 × 𝐵 ) ⊆ V
16		resmpt	⊢ ( ( 𝐴 × 𝐵 ) ⊆ V → ( ( 𝑥 ∈ V ↦ ∪ dom { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ dom { 𝑥 } ) )
17	15 16	ax-mp	⊢ ( ( 𝑥 ∈ V ↦ ∪ dom { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ dom { 𝑥 } )
18	14 17	eqtri	⊢ ( 1st ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ dom { 𝑥 } )
19	18	fmpt	⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ dom { 𝑥 } ∈ 𝐴 ↔ ( 1st ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐴 )
20	12 19	mpbi	⊢ ( 1st ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐴