Metamath Proof Explorer


Theorem pw2f1o2val

Description: Function value of the pw2f1o2 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypothesis pw2f1o2.f 𝐹 = ( 𝑥 ∈ ( 2om 𝐴 ) ↦ ( 𝑥 “ { 1o } ) )
Assertion pw2f1o2val ( 𝑋 ∈ ( 2om 𝐴 ) → ( 𝐹𝑋 ) = ( 𝑋 “ { 1o } ) )

Proof

Step Hyp Ref Expression
1 pw2f1o2.f 𝐹 = ( 𝑥 ∈ ( 2om 𝐴 ) ↦ ( 𝑥 “ { 1o } ) )
2 cnvexg ( 𝑋 ∈ ( 2om 𝐴 ) → 𝑋 ∈ V )
3 imaexg ( 𝑋 ∈ V → ( 𝑋 “ { 1o } ) ∈ V )
4 2 3 syl ( 𝑋 ∈ ( 2om 𝐴 ) → ( 𝑋 “ { 1o } ) ∈ V )
5 cnveq ( 𝑥 = 𝑋 𝑥 = 𝑋 )
6 5 imaeq1d ( 𝑥 = 𝑋 → ( 𝑥 “ { 1o } ) = ( 𝑋 “ { 1o } ) )
7 6 1 fvmptg ( ( 𝑋 ∈ ( 2om 𝐴 ) ∧ ( 𝑋 “ { 1o } ) ∈ V ) → ( 𝐹𝑋 ) = ( 𝑋 “ { 1o } ) )
8 4 7 mpdan ( 𝑋 ∈ ( 2om 𝐴 ) → ( 𝐹𝑋 ) = ( 𝑋 “ { 1o } ) )