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 ∈ B A ∧ F A ⊆ C ↔ F ∈ C A

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 ∧ F A ⊆ C ↔ F : A ⟶ C
6 1 4 5 3syl ⊢ A ∈ U ∧ B ∈ V ∧ C ⊆ B → F : A ⟶ B ∧ F A ⊆ 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 ∈ B A ↔ F : A ⟶ B
10 9 anbi1d ⊢ A ∈ U ∧ B ∈ V ∧ C ⊆ B → F ∈ B A ∧ F A ⊆ C ↔ F : A ⟶ B ∧ F A ⊆ C
11 7 1 ssexd ⊢ A ∈ U ∧ B ∈ V ∧ C ⊆ B → C ∈ V
12 11 8 elmapd ⊢ A ∈ U ∧ B ∈ V ∧ C ⊆ B → F ∈ C A ↔ F : A ⟶ C
13 6 10 12 3bitr4d ⊢ A ∈ U ∧ B ∈ V ∧ C ⊆ B → F ∈ B A ∧ F A ⊆ C ↔ F ∈ C A