Metamath Proof Explorer

Theorem k0004lem3

Description: When the value of a mapping on a singleton is known, the mapping is a completely known singleton. (Contributed by RP, 2-Apr-2021)

Ref Expression
Assertion k0004lem3 ⊢A∈U∧B∈V∧C∈B→F∈BA∧F⁡A=C↔F=AC

Proof

Step Hyp Ref Expression
1 sneq ⊢F⁡A=C→F⁡A=C
2 eqimss ⊢F⁡A=C→F⁡A⊆C
3 1 2 syl ⊢F⁡A=C→F⁡A⊆C
4 fvex ⊢F⁡A∈V
5 4 snsssn ⊢F⁡A⊆C→F⁡A=C
6 3 5 impbii ⊢F⁡A=C↔F⁡A⊆C
7 elmapfn ⊢F∈BA→FFnA
8 simpl1 ⊢A∈U∧B∈V∧C∈B∧F∈BA→A∈U
9 snidg ⊢A∈U→A∈A
10 8 9 syl ⊢A∈U∧B∈V∧C∈B∧F∈BA→A∈A
11 fnsnfv ⊢FFnA∧A∈A→F⁡A=FA
12 7 10 11 syl2an2 ⊢A∈U∧B∈V∧C∈B∧F∈BA→F⁡A=FA
13 12 sseq1d ⊢A∈U∧B∈V∧C∈B∧F∈BA→F⁡A⊆C↔FA⊆C
14 6 13 bitrid ⊢A∈U∧B∈V∧C∈B∧F∈BA→F⁡A=C↔FA⊆C
15 14 pm5.32da ⊢A∈U∧B∈V∧C∈B→F∈BA∧F⁡A=C↔F∈BA∧FA⊆C
16 snex ⊢A∈V
17 simp2 ⊢A∈U∧B∈V∧C∈B→B∈V
18 simp3 ⊢A∈U∧B∈V∧C∈B→C∈B
19 18 snssd ⊢A∈U∧B∈V∧C∈B→C⊆B
20 k0004lem2 ⊢A∈V∧B∈V∧C⊆B→F∈BA∧FA⊆C↔F∈CA
21 16 17 19 20 mp3an2i ⊢A∈U∧B∈V∧C∈B→F∈BA∧FA⊆C↔F∈CA
22 snex ⊢C∈V
23 22 16 elmap ⊢F∈CA↔F:A⟶C
24 fsng ⊢A∈U∧C∈B→F:A⟶C↔F=AC
25 24 3adant2 ⊢A∈U∧B∈V∧C∈B→F:A⟶C↔F=AC
26 23 25 bitrid ⊢A∈U∧B∈V∧C∈B→F∈CA↔F=AC
27 15 21 26 3bitrd ⊢A∈U∧B∈V∧C∈B→F∈BA∧F⁡A=C↔F=AC