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

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 ∈ B A → F Fn A
8 simpl1 ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ B ∧ F ∈ B A → A ∈ U
9 snidg ⊢ A ∈ U → A ∈ A
10 8 9 syl ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ B ∧ F ∈ B A → A ∈ A
11 fnsnfv ⊢ F Fn A ∧ A ∈ A → F ⁡ A = F A
12 7 10 11 syl2an2 ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ B ∧ F ∈ B A → F ⁡ A = F A
13 12 sseq1d ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ B ∧ F ∈ B A → F ⁡ A ⊆ C ↔ F A ⊆ C
14 6 13 bitrid ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ B ∧ F ∈ B A → F ⁡ A = C ↔ F A ⊆ C
15 14 pm5.32da ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ B → F ∈ B A ∧ F ⁡ A = C ↔ F ∈ B A ∧ F A ⊆ 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 ∈ B A ∧ F A ⊆ C ↔ F ∈ C A
21 16 17 19 20 mp3an2i ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ B → F ∈ B A ∧ F A ⊆ C ↔ F ∈ C A
22 snex ⊢ C ∈ V
23 22 16 elmap ⊢ F ∈ C A ↔ F : A ⟶ C
24 fsng ⊢ A ∈ U ∧ C ∈ B → F : A ⟶ C ↔ F = A C
25 24 3adant2 ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ B → F : A ⟶ C ↔ F = A C
26 23 25 bitrid ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ B → F ∈ C A ↔ F = A C
27 15 21 26 3bitrd ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ B → F ∈ B A ∧ F ⁡ A = C ↔ F = A C