Metamath Proof Explorer

Theorem fsetsnf1

Description: The mapping of an element of a class to a singleton function is an injection. (Contributed by AV, 13-Sep-2024)

Ref Expression
Hypotheses fsetsnf.a ⊢A=y|∃b∈By=Sb
fsetsnf.f ⊢F=x∈B⟼Sx
Assertion fsetsnf1 ⊢S∈V→F:B⟶1-1A

Proof

Step Hyp Ref Expression
1 fsetsnf.a ⊢A=y|∃b∈By=Sb
2 fsetsnf.f ⊢F=x∈B⟼Sx
3 1 2 fsetsnf ⊢S∈V→F:B⟶A
4 2 a1i ⊢m∈B∧n∈B→F=x∈B⟼Sx
5 opeq2 ⊢x=m→Sx=Sm
6 5 sneqd ⊢x=m→Sx=Sm
7 6 adantl ⊢m∈B∧n∈B∧x=m→Sx=Sm
8 simpl ⊢m∈B∧n∈B→m∈B
9 snex ⊢Sm∈V
10 9 a1i ⊢m∈B∧n∈B→Sm∈V
11 4 7 8 10 fvmptd ⊢m∈B∧n∈B→F⁡m=Sm
12 opeq2 ⊢x=n→Sx=Sn
13 12 sneqd ⊢x=n→Sx=Sn
14 13 adantl ⊢m∈B∧n∈B∧x=n→Sx=Sn
15 simpr ⊢m∈B∧n∈B→n∈B
16 snex ⊢Sn∈V
17 16 a1i ⊢m∈B∧n∈B→Sn∈V
18 4 14 15 17 fvmptd ⊢m∈B∧n∈B→F⁡n=Sn
19 11 18 eqeq12d ⊢m∈B∧n∈B→F⁡m=F⁡n↔Sm=Sn
20 19 adantl ⊢S∈V∧m∈B∧n∈B→F⁡m=F⁡n↔Sm=Sn
21 opex ⊢Sm∈V
22 21 sneqr ⊢Sm=Sn→Sm=Sn
23 opthg ⊢S∈V∧m∈B→Sm=Sn↔S=S∧m=n
24 23 adantrr ⊢S∈V∧m∈B∧n∈B→Sm=Sn↔S=S∧m=n
25 simpr ⊢S=S∧m=n→m=n
26 24 25 syl6bi ⊢S∈V∧m∈B∧n∈B→Sm=Sn→m=n
27 22 26 syl5 ⊢S∈V∧m∈B∧n∈B→Sm=Sn→m=n
28 20 27 sylbid ⊢S∈V∧m∈B∧n∈B→F⁡m=F⁡n→m=n
29 28 ralrimivva ⊢S∈V→∀m∈B∀n∈BF⁡m=F⁡n→m=n
30 dff13 ⊢F:B⟶1-1A↔F:B⟶A∧∀m∈B∀n∈BF⁡m=F⁡n→m=n
31 3 29 30 sylanbrc ⊢S∈V→F:B⟶1-1A