Theorem pw2f1o2val

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	$$⊢F=\left(x\in \left({2_{𝑜}}^A\right)⟼x^{-1}\left[\left\{1_{𝑜}\right\}\right]\right)$$
Assertion	pw2f1o2val	$$⊢X\in \left({2_{𝑜}}^A\right)\to F\left(X\right)=X^{-1}\left[\left\{1_{𝑜}\right\}\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		cnvexg	$$⊢X\in \left({2_{𝑜}}^A\right)\to X^{-1}\in \mathrm{V}$$
3		imaexg	$$⊢X^{-1}\in \mathrm{V}\to X^{-1}\left[\left\{1_{𝑜}\right\}\right]\in \mathrm{V}$$
4	2 3	syl	$$⊢X\in \left({2_{𝑜}}^A\right)\to X^{-1}\left[\left\{1_{𝑜}\right\}\right]\in \mathrm{V}$$
5		cnveq	$$⊢x=X\to x^{-1}=X^{-1}$$
6	5	imaeq1d	$$⊢x=X\to x^{-1}\left[\left\{1_{𝑜}\right\}\right]=X^{-1}\left[\left\{1_{𝑜}\right\}\right]$$
7	6 1	fvmptg	$$⊢\left(X\in \left({2_{𝑜}}^A\right)\wedge X^{-1}\left[\left\{1_{𝑜}\right\}\right]\in \mathrm{V}\right)\to F\left(X\right)=X^{-1}\left[\left\{1_{𝑜}\right\}\right]$$
8	4 7	mpdan	$$⊢X\in \left({2_{𝑜}}^A\right)\to F\left(X\right)=X^{-1}\left[\left\{1_{𝑜}\right\}\right]$$