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	⊢ 𝐹 = ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) )
Assertion	pw2f1o2val	⊢ ( 𝑋 ∈ ( 2o ↑m 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( ◡ 𝑋 “ { 1o } ) )

Proof

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