Metamath Proof Explorer

Theorem k0004lem2

Description: A mapping with a particular restricted range is also a mapping to that range. (Contributed by RP, 1-Apr-2021)

Ref Expression
Assertion k0004lem2 ⊢A∈U∧B∈V∧C⊆B→F∈BA∧FA⊆C↔F∈CA

Proof

Step Hyp Ref Expression
1 simp3 ⊢A∈U∧B∈V∧C⊆B→C⊆B
2 sseqin2 ⊢C⊆B↔B∩C=C
3 2 biimpi ⊢C⊆B→B∩C=C
4 3 eqcomd ⊢C⊆B→C=B∩C
5 k0004lem1 ⊢C=B∩C→F:A⟶B∧FA⊆C↔F:A⟶C
6 1 4 5 3syl ⊢A∈U∧B∈V∧C⊆B→F:A⟶B∧FA⊆C↔F:A⟶C
7 simp2 ⊢A∈U∧B∈V∧C⊆B→B∈V
8 simp1 ⊢A∈U∧B∈V∧C⊆B→A∈U
9 7 8 elmapd ⊢A∈U∧B∈V∧C⊆B→F∈BA↔F:A⟶B
10 9 anbi1d ⊢A∈U∧B∈V∧C⊆B→F∈BA∧FA⊆C↔F:A⟶B∧FA⊆C
11 7 1 ssexd ⊢A∈U∧B∈V∧C⊆B→C∈V
12 11 8 elmapd ⊢A∈U∧B∈V∧C⊆B→F∈CA↔F:A⟶C
13 6 10 12 3bitr4d ⊢A∈U∧B∈V∧C⊆B→F∈BA∧FA⊆C↔F∈CA