Metamath Proof Explorer


Theorem fsn2

Description: A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by NM, 19-May-2004)

Ref Expression
Hypothesis fsn2.1 𝐴 ∈ V
Assertion fsn2 ( 𝐹 : { 𝐴 } ⟶ 𝐵 ↔ ( ( 𝐹𝐴 ) ∈ 𝐵𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) )

Proof

Step Hyp Ref Expression
1 fsn2.1 𝐴 ∈ V
2 1 snid 𝐴 ∈ { 𝐴 }
3 ffvelrn ( ( 𝐹 : { 𝐴 } ⟶ 𝐵𝐴 ∈ { 𝐴 } ) → ( 𝐹𝐴 ) ∈ 𝐵 )
4 2 3 mpan2 ( 𝐹 : { 𝐴 } ⟶ 𝐵 → ( 𝐹𝐴 ) ∈ 𝐵 )
5 ffn ( 𝐹 : { 𝐴 } ⟶ 𝐵𝐹 Fn { 𝐴 } )
6 dffn3 ( 𝐹 Fn { 𝐴 } ↔ 𝐹 : { 𝐴 } ⟶ ran 𝐹 )
7 6 biimpi ( 𝐹 Fn { 𝐴 } → 𝐹 : { 𝐴 } ⟶ ran 𝐹 )
8 imadmrn ( 𝐹 “ dom 𝐹 ) = ran 𝐹
9 fndm ( 𝐹 Fn { 𝐴 } → dom 𝐹 = { 𝐴 } )
10 9 imaeq2d ( 𝐹 Fn { 𝐴 } → ( 𝐹 “ dom 𝐹 ) = ( 𝐹 “ { 𝐴 } ) )
11 8 10 eqtr3id ( 𝐹 Fn { 𝐴 } → ran 𝐹 = ( 𝐹 “ { 𝐴 } ) )
12 fnsnfv ( ( 𝐹 Fn { 𝐴 } ∧ 𝐴 ∈ { 𝐴 } ) → { ( 𝐹𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )
13 2 12 mpan2 ( 𝐹 Fn { 𝐴 } → { ( 𝐹𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )
14 11 13 eqtr4d ( 𝐹 Fn { 𝐴 } → ran 𝐹 = { ( 𝐹𝐴 ) } )
15 14 feq3d ( 𝐹 Fn { 𝐴 } → ( 𝐹 : { 𝐴 } ⟶ ran 𝐹𝐹 : { 𝐴 } ⟶ { ( 𝐹𝐴 ) } ) )
16 7 15 mpbid ( 𝐹 Fn { 𝐴 } → 𝐹 : { 𝐴 } ⟶ { ( 𝐹𝐴 ) } )
17 5 16 syl ( 𝐹 : { 𝐴 } ⟶ 𝐵𝐹 : { 𝐴 } ⟶ { ( 𝐹𝐴 ) } )
18 4 17 jca ( 𝐹 : { 𝐴 } ⟶ 𝐵 → ( ( 𝐹𝐴 ) ∈ 𝐵𝐹 : { 𝐴 } ⟶ { ( 𝐹𝐴 ) } ) )
19 snssi ( ( 𝐹𝐴 ) ∈ 𝐵 → { ( 𝐹𝐴 ) } ⊆ 𝐵 )
20 fss ( ( 𝐹 : { 𝐴 } ⟶ { ( 𝐹𝐴 ) } ∧ { ( 𝐹𝐴 ) } ⊆ 𝐵 ) → 𝐹 : { 𝐴 } ⟶ 𝐵 )
21 20 ancoms ( ( { ( 𝐹𝐴 ) } ⊆ 𝐵𝐹 : { 𝐴 } ⟶ { ( 𝐹𝐴 ) } ) → 𝐹 : { 𝐴 } ⟶ 𝐵 )
22 19 21 sylan ( ( ( 𝐹𝐴 ) ∈ 𝐵𝐹 : { 𝐴 } ⟶ { ( 𝐹𝐴 ) } ) → 𝐹 : { 𝐴 } ⟶ 𝐵 )
23 18 22 impbii ( 𝐹 : { 𝐴 } ⟶ 𝐵 ↔ ( ( 𝐹𝐴 ) ∈ 𝐵𝐹 : { 𝐴 } ⟶ { ( 𝐹𝐴 ) } ) )
24 fvex ( 𝐹𝐴 ) ∈ V
25 1 24 fsn ( 𝐹 : { 𝐴 } ⟶ { ( 𝐹𝐴 ) } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } )
26 25 anbi2i ( ( ( 𝐹𝐴 ) ∈ 𝐵𝐹 : { 𝐴 } ⟶ { ( 𝐹𝐴 ) } ) ↔ ( ( 𝐹𝐴 ) ∈ 𝐵𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) )
27 23 26 bitri ( 𝐹 : { 𝐴 } ⟶ 𝐵 ↔ ( ( 𝐹𝐴 ) ∈ 𝐵𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) )