Theorem pw2f1o2val2

Description: Membership in a mapped set under 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	pw2f1o2val2	⊢ ( ( 𝑋 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝑋 ‘ 𝑌 ) = 1o ) )

Proof

Step	Hyp	Ref	Expression
1		pw2f1o2.f	⊢ 𝐹 = ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) )
2	1	pw2f1o2val	⊢ ( 𝑋 ∈ ( 2o ↑m 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( ◡ 𝑋 “ { 1o } ) )
3	2	eleq2d	⊢ ( 𝑋 ∈ ( 2o ↑m 𝐴 ) → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ 𝑌 ∈ ( ◡ 𝑋 “ { 1o } ) ) )
4	3	adantr	⊢ ( ( 𝑋 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ 𝑌 ∈ ( ◡ 𝑋 “ { 1o } ) ) )
5		elmapi	⊢ ( 𝑋 ∈ ( 2o ↑m 𝐴 ) → 𝑋 : 𝐴 ⟶ 2o )
6		ffn	⊢ ( 𝑋 : 𝐴 ⟶ 2o → 𝑋 Fn 𝐴 )
7		fniniseg	⊢ ( 𝑋 Fn 𝐴 → ( 𝑌 ∈ ( ◡ 𝑋 “ { 1o } ) ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝑋 ‘ 𝑌 ) = 1o ) ) )
8	5 6 7	3syl	⊢ ( 𝑋 ∈ ( 2o ↑m 𝐴 ) → ( 𝑌 ∈ ( ◡ 𝑋 “ { 1o } ) ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝑋 ‘ 𝑌 ) = 1o ) ) )
9	8	baibd	⊢ ( ( 𝑋 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ ( ◡ 𝑋 “ { 1o } ) ↔ ( 𝑋 ‘ 𝑌 ) = 1o ) )
10	4 9	bitrd	⊢ ( ( 𝑋 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝑋 ‘ 𝑌 ) = 1o ) )