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		ffvelcdm	⊢ ( ( 𝐹 : { 𝐴 } ⟶ 𝐵 ∧ 𝐴 ∈ { 𝐴 } ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 )
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	⊢ ( 𝐹 : { 𝐴 } ⟶ 𝐵 ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) )

Metamath Proof Explorer

Theorem fsn2

Proof