funop

Description: An ordered pair is a function iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020) 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	\|- X e. _V
	funopsn.y	\|- Y e. _V
Assertion	funop	\|- ( Fun <. X , Y >. <-> E. a ( X = { a } /\ <. X , Y >. = { <. a , a >. } ) )

Proof

Step	Hyp	Ref	Expression
1		funopsn.x	\|- X e. _V
2		funopsn.y	\|- Y e. _V
3		eqid	\|- <. X , Y >. = <. X , Y >.
4	1 2	funopsn	\|- ( ( Fun <. X , Y >. /\ <. X , Y >. = <. X , Y >. ) -> E. a ( X = { a } /\ <. X , Y >. = { <. a , a >. } ) )
5	3 4	mpan2	\|- ( Fun <. X , Y >. -> E. a ( X = { a } /\ <. X , Y >. = { <. a , a >. } ) )
6		vex	\|- a e. _V
7	6 6	funsn	\|- Fun { <. a , a >. }
8		funeq	\|- ( <. X , Y >. = { <. a , a >. } -> ( Fun <. X , Y >. <-> Fun { <. a , a >. } ) )
9	7 8	mpbiri	\|- ( <. X , Y >. = { <. a , a >. } -> Fun <. X , Y >. )
10	9	adantl	\|- ( ( X = { a } /\ <. X , Y >. = { <. a , a >. } ) -> Fun <. X , Y >. )
11	10	exlimiv	\|- ( E. a ( X = { a } /\ <. X , Y >. = { <. a , a >. } ) -> Fun <. X , Y >. )
12	5 11	impbii	\|- ( Fun <. X , Y >. <-> E. a ( X = { a } /\ <. X , Y >. = { <. a , a >. } ) )

Metamath Proof Explorer

Theorem funop

Proof