Metamath Proof Explorer


Theorem 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 B I × x
pwssnf1o.c C = Base Y
Assertion pwssnf1o R V I W F : B 1-1 onto C

Proof

Step Hyp Ref Expression
1 pwssnf1o.y Y = R 𝑠 I
2 pwssnf1o.b B = Base R
3 pwssnf1o.f F = x B I × x
4 pwssnf1o.c C = Base Y
5 2 fvexi B V
6 simpr R V I W I W
7 3 mapsnf1o B V I W F : B 1-1 onto B I
8 5 6 7 sylancr R V I W F : B 1-1 onto B I
9 snex I V
10 1 2 pwsbas R V I V B I = Base Y
11 9 10 mpan2 R V B I = Base Y
12 11 adantr R V I W B I = Base Y
13 4 12 eqtr4id R V I W C = B I
14 13 f1oeq3d R V I W F : B 1-1 onto C F : B 1-1 onto B I
15 8 14 mpbird R V I W F : B 1-1 onto C