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 } ) ) |
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 } ) ) |