This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ 𝐹 = ( 𝑥 ∈ ( 2_o ↑_m 𝐴 ) ↦ ( ^◡ 𝑥 “ { 1_o } ) )
	Assertion	pw2f1o2val2	⊢ ( ( 𝑋 ∈ ( 2_o ↑_m 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝑋 ‘ 𝑌 ) = 1_o ) )

Proof

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