Theorem pwssnf1o

Description: Triviality of singleton powers: set equipollence. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypotheses	pwssnf1o.y	$$⊢Y=R{\uparrow }_{𝑠}\left\{I\right\}$$
	pwssnf1o.b	$$⊢B={\mathrm{Base}}_R$$
	pwssnf1o.f	$$⊢F=\left(x\in B⟼\left\{I\right\}\times \left\{x\right\}\right)$$
	pwssnf1o.c	$$⊢C={\mathrm{Base}}_Y$$
Assertion	pwssnf1o	$$⊢\left(R\in V\wedge I\in W\right)\to F:B\underset{1-1\; onto}{⟶}C$$

Proof

Step	Hyp	Ref	Expression
1		pwssnf1o.y	$$⊢Y=R{\uparrow }_{𝑠}\left\{I\right\}$$
2		pwssnf1o.b	$$⊢B={\mathrm{Base}}_R$$
3		pwssnf1o.f	$$⊢F=\left(x\in B⟼\left\{I\right\}\times \left\{x\right\}\right)$$
4		pwssnf1o.c	$$⊢C={\mathrm{Base}}_Y$$
5	2	fvexi	$$⊢B\in \mathrm{V}$$
6		simpr	$$⊢\left(R\in V\wedge I\in W\right)\to I\in W$$
7	3	mapsnf1o	$$⊢\left(B\in \mathrm{V}\wedge I\in W\right)\to F:B\underset{1-1\; onto}{⟶}{B}^{\left\{I\right\}}$$
8	5 6 7	sylancr	$$⊢\left(R\in V\wedge I\in W\right)\to F:B\underset{1-1\; onto}{⟶}{B}^{\left\{I\right\}}$$
9		snex	$$⊢\left\{I\right\}\in \mathrm{V}$$
10	1 2	pwsbas	$$⊢\left(R\in V\wedge \left\{I\right\}\in \mathrm{V}\right)\to B^{\left\{I\right\}}={\mathrm{Base}}_Y$$
11	9 10	mpan2	$$⊢R\in V\to B^{\left\{I\right\}}={\mathrm{Base}}_Y$$
12	11	adantr	$$⊢\left(R\in V\wedge I\in W\right)\to B^{\left\{I\right\}}={\mathrm{Base}}_Y$$
13	4 12	eqtr4id	$$⊢\left(R\in V\wedge I\in W\right)\to C=B^{\left\{I\right\}}$$
14	13	f1oeq3d	$$⊢\left(R\in V\wedge I\in W\right)\to \left(F:B\underset{1-1\; onto}{⟶}C\leftrightarrow F:B\underset{1-1\; onto}{⟶}{B}^{\left\{I\right\}}\right)$$
15	8 14	mpbird	$$⊢\left(R\in V\wedge I\in W\right)\to F:B\underset{1-1\; onto}{⟶}C$$