df1st2

Description: An alternate possible definition of the 1st function. (Contributed by NM, 14-Oct-2004) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	df1st2	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } = ( 1^st ↾ ( V × V ) )

Step	Hyp	Ref	Expression
1		fo1st	⊢ 1^st : V –onto→ V
2		fofn	⊢ ( 1^st : V –onto→ V → 1^st Fn V )
3	1 2	ax-mp	⊢ 1^st Fn V
4		dffn5	⊢ ( 1^st Fn V ↔ 1^st = ( 𝑤 ∈ V ↦ ( 1^st ‘ 𝑤 ) ) )
5	3 4	mpbi	⊢ 1^st = ( 𝑤 ∈ V ↦ ( 1^st ‘ 𝑤 ) )
6		mptv	⊢ ( 𝑤 ∈ V ↦ ( 1^st ‘ 𝑤 ) ) = { ⟨ 𝑤 , 𝑧 ⟩ ∣ 𝑧 = ( 1^st ‘ 𝑤 ) }
7	5 6	eqtri	⊢ 1^st = { ⟨ 𝑤 , 𝑧 ⟩ ∣ 𝑧 = ( 1^st ‘ 𝑤 ) }
8	7	reseq1i	⊢ ( 1^st ↾ ( V × V ) ) = ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ 𝑧 = ( 1^st ‘ 𝑤 ) } ↾ ( V × V ) )
9		resopab	⊢ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ 𝑧 = ( 1^st ‘ 𝑤 ) } ↾ ( V × V ) ) = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( V × V ) ∧ 𝑧 = ( 1^st ‘ 𝑤 ) ) }
10		vex	⊢ 𝑥 ∈ V
11		vex	⊢ 𝑦 ∈ V
12	10 11	op1std	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝑤 ) = 𝑥 )
13	12	eqeq2d	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 = ( 1^st ‘ 𝑤 ) ↔ 𝑧 = 𝑥 ) )
14	13	dfoprab3	⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( V × V ) ∧ 𝑧 = ( 1^st ‘ 𝑤 ) ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 }
15	8 9 14	3eqtrri	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } = ( 1^st ↾ ( V × V ) )

Metamath Proof Explorer