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	biimpri	⊢ ( 𝑦 ∈ 𝐴 → ∪ dom { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐴 )
6	5	adantr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ∪ dom { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐴 )
7	6	rgen2	⊢ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∪ dom { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐴
8		sneq	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → { 𝑥 } = { ⟨ 𝑦 , 𝑧 ⟩ } )
9	8	dmeqd	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → dom { 𝑥 } = dom { ⟨ 𝑦 , 𝑧 ⟩ } )
10	9	unieqd	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ∪ dom { 𝑥 } = ∪ dom { ⟨ 𝑦 , 𝑧 ⟩ } )
11	10	eleq1d	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ∪ dom { 𝑥 } ∈ 𝐴 ↔ ∪ dom { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐴 ) )
12	11	ralxp	⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ dom { 𝑥 } ∈ 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∪ dom { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐴 )
13	7 12	mpbir	⊢ ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ dom { 𝑥 } ∈ 𝐴
14		df-1st	⊢ 1st = ( 𝑥 ∈ V ↦ ∪ dom { 𝑥 } )
15	14	reseq1i	⊢ ( 1st ↾ ( 𝐴 × 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ ∪ dom { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) )
16		ssv	⊢ ( 𝐴 × 𝐵 ) ⊆ V
17		resmpt	⊢ ( ( 𝐴 × 𝐵 ) ⊆ V → ( ( 𝑥 ∈ V ↦ ∪ dom { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ dom { 𝑥 } ) )
18	16 17	ax-mp	⊢ ( ( 𝑥 ∈ V ↦ ∪ dom { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ dom { 𝑥 } )
19	15 18	eqtri	⊢ ( 1st ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ dom { 𝑥 } )
20	19	fmpt	⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ dom { 𝑥 } ∈ 𝐴 ↔ ( 1st ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐴 )
21	13 20	mpbi	⊢ ( 1st ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐴