This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mapsnf1o2

Description: Explicit bijection between a set and its singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015)

Ref Expression
Hypotheses mapsncnv.s ⊢ S = X
mapsncnv.b ⊢ B ∈ V
mapsncnv.x ⊢ X ∈ V
mapsncnv.f ⊢ F = x ∈ B S ⟼ x ⁡ X
Assertion mapsnf1o2 ⊢ F : B S ⟶ 1-1 onto B

Proof

Step Hyp Ref Expression
1 mapsncnv.s ⊢ S = X
2 mapsncnv.b ⊢ B ∈ V
3 mapsncnv.x ⊢ X ∈ V
4 mapsncnv.f ⊢ F = x ∈ B S ⟼ x ⁡ X
5 fvex ⊢ x ⁡ X ∈ V
6 5 4 fnmpti ⊢ F Fn B S
7 snex ⊢ X ∈ V
8 1 7 eqeltri ⊢ S ∈ V
9 snex ⊢ y ∈ V
10 8 9 xpex ⊢ S × y ∈ V
11 1 2 3 4 mapsncnv ⊢ F -1 = y ∈ B ⟼ S × y
12 10 11 fnmpti ⊢ F -1 Fn B
13 dff1o4 ⊢ F : B S ⟶ 1-1 onto B ↔ F Fn B S ∧ F -1 Fn B
14 6 12 13 mpbir2an ⊢ F : B S ⟶ 1-1 onto B