pwssnf1o

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

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

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

Metamath Proof Explorer