This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fliftfund

Description: The function F is the unique function defined by FA = B , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016)

		Ref	Expression
	Hypotheses	flift.1	\|- F = ran ( x e. X \|-> <. A , B >. )
		flift.2	\|- ( ( ph /\ x e. X ) -> A e. R )
		flift.3	\|- ( ( ph /\ x e. X ) -> B e. S )
		fliftfun.4	\|- ( x = y -> A = C )
		fliftfun.5	\|- ( x = y -> B = D )
		fliftfund.6	\|- ( ( ph /\ ( x e. X /\ y e. X /\ A = C ) ) -> B = D )
	Assertion	fliftfund	\|- ( ph -> Fun F )

Proof

Step	Hyp	Ref	Expression
1		flift.1	\|- F = ran ( x e. X \|-> <. A , B >. )
2		flift.2	\|- ( ( ph /\ x e. X ) -> A e. R )
3		flift.3	\|- ( ( ph /\ x e. X ) -> B e. S )
4		fliftfun.4	\|- ( x = y -> A = C )
5		fliftfun.5	\|- ( x = y -> B = D )
6		fliftfund.6	\|- ( ( ph /\ ( x e. X /\ y e. X /\ A = C ) ) -> B = D )
7	6	3exp2	\|- ( ph -> ( x e. X -> ( y e. X -> ( A = C -> B = D ) ) ) )
8	7	imp32	\|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( A = C -> B = D ) )
9	8	ralrimivva	\|- ( ph -> A. x e. X A. y e. X ( A = C -> B = D ) )
10	1 2 3 4 5	fliftfun	\|- ( ph -> ( Fun F <-> A. x e. X A. y e. X ( A = C -> B = D ) ) )
11	9 10	mpbird	\|- ( ph -> Fun F )