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

Metamath Proof Explorer

Theorem mapsnconst

Description: Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Hypotheses mapsncnv.s ⊢ S = X
mapsncnv.b ⊢ B ∈ V
mapsncnv.x ⊢ X ∈ V
Assertion mapsnconst ⊢ F ∈ B S → F = S × F ⁡ X

Proof

Step Hyp Ref Expression
1 mapsncnv.s ⊢ S = X
2 mapsncnv.b ⊢ B ∈ V
3 mapsncnv.x ⊢ X ∈ V
4 snex ⊢ X ∈ V
5 2 4 elmap ⊢ F ∈ B X ↔ F : X ⟶ B
6 3 fsn2 ⊢ F : X ⟶ B ↔ F ⁡ X ∈ B ∧ F = X F ⁡ X
7 6 simprbi ⊢ F : X ⟶ B → F = X F ⁡ X
8 1 xpeq1i ⊢ S × F ⁡ X = X × F ⁡ X
9 fvex ⊢ F ⁡ X ∈ V
10 3 9 xpsn ⊢ X × F ⁡ X = X F ⁡ X
11 8 10 eqtr2i ⊢ X F ⁡ X = S × F ⁡ X
12 7 11 eqtrdi ⊢ F : X ⟶ B → F = S × F ⁡ X
13 5 12 sylbi ⊢ F ∈ B X → F = S × F ⁡ X
14 1 oveq2i ⊢ B S = B X
15 13 14 eleq2s ⊢ F ∈ B S → F = S × F ⁡ X