Metamath Proof Explorer


Theorem 2ndinr

Description: The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022)

Ref Expression
Assertion 2ndinr ( 𝑋𝑉 → ( 2nd ‘ ( inr ‘ 𝑋 ) ) = 𝑋 )

Proof

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