Theorem funopsn

Description: If a function is an ordered pair then it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020) (Proof shortened by AV, 15-Jul-2021) (Proof shortened by Eric Schmidt, 9-May-2026) A function is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a function is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is funsng , as relsnopg is to relop . (New usage is discouraged.)

	Ref	Expression
Hypotheses	funopsn.x	⊢ 𝑋 ∈ V
	funopsn.y	⊢ 𝑌 ∈ V
Assertion	funopsn	⊢ ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		funopsn.x	⊢ 𝑋 ∈ V
2		funopsn.y	⊢ 𝑌 ∈ V
3		funiun	⊢ ( Fun 𝐹 → 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
4		eqeq1	⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ↔ ⟨ 𝑋 , 𝑌 ⟩ = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) )
5		eqcom	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ↔ ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ )
6	4 5	bitrdi	⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ↔ ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ ) )
7		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
8	7 1 2	iunopeqop	⊢ ( ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ → ∃ 𝑎 dom 𝐹 = { 𝑎 } )
9	6 8	biimtrdi	⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } → ∃ 𝑎 dom 𝐹 = { 𝑎 } ) )
10	9	imp	⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) → ∃ 𝑎 dom 𝐹 = { 𝑎 } )
11		iuneq1	⊢ ( dom 𝐹 = { 𝑎 } → ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = ∪ 𝑥 ∈ { 𝑎 } { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
12		vex	⊢ 𝑎 ∈ V
13		id	⊢ ( 𝑥 = 𝑎 → 𝑥 = 𝑎 )
14		fveq2	⊢ ( 𝑥 = 𝑎 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑎 ) )
15	13 14	opeq12d	⊢ ( 𝑥 = 𝑎 → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ = ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ )
16	15	sneqd	⊢ ( 𝑥 = 𝑎 → { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } )
17	12 16	iunxsn	⊢ ∪ 𝑥 ∈ { 𝑎 } { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ }
18	11 17	eqtrdi	⊢ ( dom 𝐹 = { 𝑎 } → ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } )
19	18	eqeq2d	⊢ ( dom 𝐹 = { 𝑎 } → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ↔ 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) )
20	19	adantl	⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ dom 𝐹 = { 𝑎 } ) → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ↔ 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) )
21		eqeq1	⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ↔ ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) )
22		eqcom	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ↔ { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ )
23		fvex	⊢ ( 𝐹 ‘ 𝑎 ) ∈ V
24	12 23	snopeqop	⊢ ( { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } = ⟨ 𝑋 , 𝑌 ⟩ ↔ ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) )
25	22 24	sylbb	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } → ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) )
26	21 25	biimtrdi	⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } → ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) ) )
27		simpr3	⊢ ( ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ∧ ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) ) → 𝑋 = { 𝑎 } )
28		simp1	⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → 𝑎 = ( 𝐹 ‘ 𝑎 ) )
29	28	eqcomd	⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → ( 𝐹 ‘ 𝑎 ) = 𝑎 )
30	29	opeq2d	⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ = ⟨ 𝑎 , 𝑎 ⟩ )
31	30	sneqd	⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } = { ⟨ 𝑎 , 𝑎 ⟩ } )
32	31	eqeq2d	⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ↔ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
33	32	biimpac	⊢ ( ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ∧ ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) ) → 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } )
34	27 33	jca	⊢ ( ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ∧ ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) ) → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
35	34	ex	⊢ ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } → ( ( 𝑎 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑋 = 𝑌 ∧ 𝑋 = { 𝑎 } ) → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
36	26 35	sylcom	⊢ ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
37	36	adantr	⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ dom 𝐹 = { 𝑎 } ) → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
38	20 37	sylbid	⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ dom 𝐹 = { 𝑎 } ) → ( 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
39	38	impancom	⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) → ( dom 𝐹 = { 𝑎 } → ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
40	39	eximdv	⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) → ( ∃ 𝑎 dom 𝐹 = { 𝑎 } → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) ) )
41	10 40	mpd	⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹 { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
42	3 41	sylan2	⊢ ( ( 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ∧ Fun 𝐹 ) → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
43	42	ancoms	⊢ ( ( Fun 𝐹 ∧ 𝐹 = ⟨ 𝑋 , 𝑌 ⟩ ) → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ 𝐹 = { ⟨ 𝑎 , 𝑎 ⟩ } ) )