fsn

Description: A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 10-Dec-2003)

	Ref	Expression
Hypotheses	fsn.1	⊢ 𝐴 ∈ V
	fsn.2	⊢ 𝐵 ∈ V
Assertion	fsn	⊢ ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , 𝐵 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		fsn.1	⊢ 𝐴 ∈ V
2		fsn.2	⊢ 𝐵 ∈ V
3		opelf	⊢ ( ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐵 } ) )
4		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
5		velsn	⊢ ( 𝑦 ∈ { 𝐵 } ↔ 𝑦 = 𝐵 )
6	4 5	anbi12i	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐵 } ) ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
7	3 6	sylib	⊢ ( ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
8	7	ex	⊢ ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) )
9	1	snid	⊢ 𝐴 ∈ { 𝐴 }
10		feu	⊢ ( ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } ∧ 𝐴 ∈ { 𝐴 } ) → ∃! 𝑦 ∈ { 𝐵 } ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 )
11	9 10	mpan2	⊢ ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } → ∃! 𝑦 ∈ { 𝐵 } ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 )
12	5	anbi1i	⊢ ( ( 𝑦 ∈ { 𝐵 } ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ↔ ( 𝑦 = 𝐵 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) )
13		opeq2	⊢ ( 𝑦 = 𝐵 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
14	13	eleq1d	⊢ ( 𝑦 = 𝐵 → ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ) )
15	14	pm5.32i	⊢ ( ( 𝑦 = 𝐵 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ↔ ( 𝑦 = 𝐵 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ) )
16	15	biancomi	⊢ ( ( 𝑦 = 𝐵 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ∧ 𝑦 = 𝐵 ) )
17	12 16	bitr2i	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑦 ∈ { 𝐵 } ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) )
18	17	eubii	⊢ ( ∃! 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ∧ 𝑦 = 𝐵 ) ↔ ∃! 𝑦 ( 𝑦 ∈ { 𝐵 } ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) )
19	2	eueqi	⊢ ∃! 𝑦 𝑦 = 𝐵
20	19	biantru	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 𝑦 = 𝐵 ) )
21		euanv	⊢ ( ∃! 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ∧ 𝑦 = 𝐵 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 𝑦 = 𝐵 ) )
22	20 21	bitr4i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ↔ ∃! 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ∧ 𝑦 = 𝐵 ) )
23		df-reu	⊢ ( ∃! 𝑦 ∈ { 𝐵 } ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ↔ ∃! 𝑦 ( 𝑦 ∈ { 𝐵 } ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) )
24	18 22 23	3bitr4i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ↔ ∃! 𝑦 ∈ { 𝐵 } ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 )
25	11 24	sylibr	⊢ ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 )
26		opeq12	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
27	26	eleq1d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ) )
28	25 27	syl5ibrcom	⊢ ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
29	8 28	impbid	⊢ ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) )
30		opex	⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
31	30	elsn	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
32	1 2	opth2	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
33	31 32	bitr2i	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } )
34	29 33	bitrdi	⊢ ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
35	34	alrimivv	⊢ ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } → ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
36		frel	⊢ ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } → Rel 𝐹 )
37	1 2	relsnop	⊢ Rel { ⟨ 𝐴 , 𝐵 ⟩ }
38		eqrel	⊢ ( ( Rel 𝐹 ∧ Rel { ⟨ 𝐴 , 𝐵 ⟩ } ) → ( 𝐹 = { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) )
39	36 37 38	sylancl	⊢ ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } → ( 𝐹 = { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) )
40	35 39	mpbird	⊢ ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } → 𝐹 = { ⟨ 𝐴 , 𝐵 ⟩ } )
41	1 2	f1osn	⊢ { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 }
42		f1oeq1	⊢ ( 𝐹 = { ⟨ 𝐴 , 𝐵 ⟩ } → ( 𝐹 : { 𝐴 } –1-1-onto→ { 𝐵 } ↔ { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ) )
43	41 42	mpbiri	⊢ ( 𝐹 = { ⟨ 𝐴 , 𝐵 ⟩ } → 𝐹 : { 𝐴 } –1-1-onto→ { 𝐵 } )
44		f1of	⊢ ( 𝐹 : { 𝐴 } –1-1-onto→ { 𝐵 } → 𝐹 : { 𝐴 } ⟶ { 𝐵 } )
45	43 44	syl	⊢ ( 𝐹 = { ⟨ 𝐴 , 𝐵 ⟩ } → 𝐹 : { 𝐴 } ⟶ { 𝐵 } )
46	40 45	impbii	⊢ ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , 𝐵 ⟩ } )

Metamath Proof Explorer

Theorem fsn

Proof