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 ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐹 ∈ ( 𝐵 ↑m { 𝐴 } ) ∧ ( 𝐹 ‘ 𝐴 ) = 𝐶 ) ↔ 𝐹 = { ⟨ 𝐴 , 𝐶 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 sneq ⊢ ( ( 𝐹 ‘ 𝐴 ) = 𝐶 → { ( 𝐹 ‘ 𝐴 ) } = { 𝐶 } )
2 eqimss ⊢ ( { ( 𝐹 ‘ 𝐴 ) } = { 𝐶 } → { ( 𝐹 ‘ 𝐴 ) } ⊆ { 𝐶 } )
3 1 2 syl ⊢ ( ( 𝐹 ‘ 𝐴 ) = 𝐶 → { ( 𝐹 ‘ 𝐴 ) } ⊆ { 𝐶 } )
4 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
5 4 snsssn ⊢ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ { 𝐶 } → ( 𝐹 ‘ 𝐴 ) = 𝐶 )
6 3 5 impbii ⊢ ( ( 𝐹 ‘ 𝐴 ) = 𝐶 ↔ { ( 𝐹 ‘ 𝐴 ) } ⊆ { 𝐶 } )
7 elmapfn ⊢ ( 𝐹 ∈ ( 𝐵 ↑m { 𝐴 } ) → 𝐹 Fn { 𝐴 } )
8 simpl1 ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝐹 ∈ ( 𝐵 ↑m { 𝐴 } ) ) → 𝐴 ∈ 𝑈 )
9 snidg ⊢ ( 𝐴 ∈ 𝑈 → 𝐴 ∈ { 𝐴 } )
10 8 9 syl ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝐹 ∈ ( 𝐵 ↑m { 𝐴 } ) ) → 𝐴 ∈ { 𝐴 } )
11 fnsnfv ⊢ ( ( 𝐹 Fn { 𝐴 } ∧ 𝐴 ∈ { 𝐴 } ) → { ( 𝐹 ‘ 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )
12 7 10 11 syl2an2 ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝐹 ∈ ( 𝐵 ↑m { 𝐴 } ) ) → { ( 𝐹 ‘ 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )
13 12 sseq1d ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝐹 ∈ ( 𝐵 ↑m { 𝐴 } ) ) → ( { ( 𝐹 ‘ 𝐴 ) } ⊆ { 𝐶 } ↔ ( 𝐹 “ { 𝐴 } ) ⊆ { 𝐶 } ) )
14 6 13 syl5bb ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝐹 ∈ ( 𝐵 ↑m { 𝐴 } ) ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐶 ↔ ( 𝐹 “ { 𝐴 } ) ⊆ { 𝐶 } ) )
15 14 pm5.32da ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐹 ∈ ( 𝐵 ↑m { 𝐴 } ) ∧ ( 𝐹 ‘ 𝐴 ) = 𝐶 ) ↔ ( 𝐹 ∈ ( 𝐵 ↑m { 𝐴 } ) ∧ ( 𝐹 “ { 𝐴 } ) ⊆ { 𝐶 } ) ) )
16 snex ⊢ { 𝐴 } ∈ V
17 simp2 ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → 𝐵 ∈ 𝑉 )
18 simp3 ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
19 18 snssd ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → { 𝐶 } ⊆ 𝐵 )
20 k0004lem2 ⊢ ( ( { 𝐴 } ∈ V ∧ 𝐵 ∈ 𝑉 ∧ { 𝐶 } ⊆ 𝐵 ) → ( ( 𝐹 ∈ ( 𝐵 ↑m { 𝐴 } ) ∧ ( 𝐹 “ { 𝐴 } ) ⊆ { 𝐶 } ) ↔ 𝐹 ∈ ( { 𝐶 } ↑m { 𝐴 } ) ) )
21 16 17 19 20 mp3an2i ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐹 ∈ ( 𝐵 ↑m { 𝐴 } ) ∧ ( 𝐹 “ { 𝐴 } ) ⊆ { 𝐶 } ) ↔ 𝐹 ∈ ( { 𝐶 } ↑m { 𝐴 } ) ) )
22 snex ⊢ { 𝐶 } ∈ V
23 22 16 elmap ⊢ ( 𝐹 ∈ ( { 𝐶 } ↑m { 𝐴 } ) ↔ 𝐹 : { 𝐴 } ⟶ { 𝐶 } )
24 fsng ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐹 : { 𝐴 } ⟶ { 𝐶 } ↔ 𝐹 = { ⟨ 𝐴 , 𝐶 ⟩ } ) )
25 24 3adant2 ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐹 : { 𝐴 } ⟶ { 𝐶 } ↔ 𝐹 = { ⟨ 𝐴 , 𝐶 ⟩ } ) )
26 23 25 syl5bb ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐹 ∈ ( { 𝐶 } ↑m { 𝐴 } ) ↔ 𝐹 = { ⟨ 𝐴 , 𝐶 ⟩ } ) )
27 15 21 26 3bitrd ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐹 ∈ ( 𝐵 ↑m { 𝐴 } ) ∧ ( 𝐹 ‘ 𝐴 ) = 𝐶 ) ↔ 𝐹 = { ⟨ 𝐴 , 𝐶 ⟩ } ) )