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	$⊢ F = (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}])$
	Assertion	pw2f1o2val2	$⊢ (X \in ({2_{𝑜}}^{A}) \land Y \in A) \to (Y \in F (X) \leftrightarrow X (Y) = 1_{𝑜})$

Proof

Step	Hyp	Ref	Expression
1		pw2f1o2.f	$⊢ F = (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}])$
2	1	pw2f1o2val	$⊢ X \in ({2_{𝑜}}^{A}) \to F (X) = X^{-1} [\{1_{𝑜}\}]$
3	2	eleq2d	$⊢ X \in ({2_{𝑜}}^{A}) \to (Y \in F (X) \leftrightarrow Y \in X^{-1} [\{1_{𝑜}\}])$
4	3	adantr	$⊢ (X \in ({2_{𝑜}}^{A}) \land Y \in A) \to (Y \in F (X) \leftrightarrow Y \in X^{-1} [\{1_{𝑜}\}])$
5		elmapi	$⊢ X \in ({2_{𝑜}}^{A}) \to X : A ⟶ 2_{𝑜}$
6		ffn	$⊢ X : A ⟶ 2_{𝑜} \to X Fn A$
7		fniniseg	$⊢ X Fn A \to (Y \in X^{-1} [\{1_{𝑜}\}] \leftrightarrow (Y \in A \land X (Y) = 1_{𝑜}))$
8	5 6 7	3syl	$⊢ X \in ({2_{𝑜}}^{A}) \to (Y \in X^{-1} [\{1_{𝑜}\}] \leftrightarrow (Y \in A \land X (Y) = 1_{𝑜}))$
9	8	baibd	$⊢ (X \in ({2_{𝑜}}^{A}) \land Y \in A) \to (Y \in X^{-1} [\{1_{𝑜}\}] \leftrightarrow X (Y) = 1_{𝑜})$
10	4 9	bitrd	$⊢ (X \in ({2_{𝑜}}^{A}) \land Y \in A) \to (Y \in F (X) \leftrightarrow X (Y) = 1_{𝑜})$