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

Metamath Proof Explorer

Theorem mapsnf1o3

Description: Explicit bijection in the reverse of mapsnf1o2 . (Contributed by Stefan O'Rear, 24-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 mapsncnv.s ⊢ S = X
2 mapsncnv.b ⊢ B ∈ V
3 mapsncnv.x ⊢ X ∈ V
4 mapsnf1o3.f ⊢ F = y ∈ B ⟼ S × y
5 eqid ⊢ x ∈ B S ⟼ x ⁡ X = x ∈ B S ⟼ x ⁡ X
6 1 2 3 5 mapsnf1o2 ⊢ x ∈ B S ⟼ x ⁡ X : B S ⟶ 1-1 onto B
7 f1ocnv ⊢ x ∈ B S ⟼ x ⁡ X : B S ⟶ 1-1 onto B → x ∈ B S ⟼ x ⁡ X -1 : B ⟶ 1-1 onto B S
8 6 7 ax-mp ⊢ x ∈ B S ⟼ x ⁡ X -1 : B ⟶ 1-1 onto B S
9 1 2 3 5 mapsncnv ⊢ x ∈ B S ⟼ x ⁡ X -1 = y ∈ B ⟼ S × y
10 4 9 eqtr4i ⊢ F = x ∈ B S ⟼ x ⁡ X -1
11 f1oeq1 ⊢ F = x ∈ B S ⟼ x ⁡ X -1 → F : B ⟶ 1-1 onto B S ↔ x ∈ B S ⟼ x ⁡ X -1 : B ⟶ 1-1 onto B S
12 10 11 ax-mp ⊢ F : B ⟶ 1-1 onto B S ↔ x ∈ B S ⟼ x ⁡ X -1 : B ⟶ 1-1 onto B S
13 8 12 mpbir ⊢ F : B ⟶ 1-1 onto B S