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

Proof

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