1stinr

Description: The first component of the value of a right injection is 1o . (Contributed by AV, 27-Jun-2022)

		Ref	Expression
	Assertion	1stinr	⊢ ( 𝑋 ∈ 𝑉 → ( 1^st ‘ ( inr ‘ 𝑋 ) ) = 1_o )

Step	Hyp	Ref	Expression
1		df-inr	⊢ inr = ( 𝑥 ∈ V ↦ ⟨ 1_o , 𝑥 ⟩ )
2		opeq2	⊢ ( 𝑥 = 𝑋 → ⟨ 1_o , 𝑥 ⟩ = ⟨ 1_o , 𝑋 ⟩ )
3		elex	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ V )
4		opex	⊢ ⟨ 1_o , 𝑋 ⟩ ∈ V
5	4	a1i	⊢ ( 𝑋 ∈ 𝑉 → ⟨ 1_o , 𝑋 ⟩ ∈ V )
6	1 2 3 5	fvmptd3	⊢ ( 𝑋 ∈ 𝑉 → ( inr ‘ 𝑋 ) = ⟨ 1_o , 𝑋 ⟩ )
7	6	fveq2d	⊢ ( 𝑋 ∈ 𝑉 → ( 1^st ‘ ( inr ‘ 𝑋 ) ) = ( 1^st ‘ ⟨ 1_o , 𝑋 ⟩ ) )
8		1oex	⊢ 1_o ∈ V
9		op1stg	⊢ ( ( 1_o ∈ V ∧ 𝑋 ∈ 𝑉 ) → ( 1^st ‘ ⟨ 1_o , 𝑋 ⟩ ) = 1_o )
10	8 9	mpan	⊢ ( 𝑋 ∈ 𝑉 → ( 1^st ‘ ⟨ 1_o , 𝑋 ⟩ ) = 1_o )
11	7 10	eqtrd	⊢ ( 𝑋 ∈ 𝑉 → ( 1^st ‘ ( inr ‘ 𝑋 ) ) = 1_o )

Metamath Proof Explorer