fundif

Description: A function with removed elements is still a function. (Contributed by AV, 7-Jun-2021)

		Ref	Expression
	Assertion	fundif	$⊢ Fun F \to Fun (F ∖ A)$

Step	Hyp	Ref	Expression
1		reldif	$⊢ Rel F \to Rel (F ∖ A)$
2		brdif	$⊢ x (F ∖ A) y \leftrightarrow (x F y \land \neg x A y)$
3		brdif	$⊢ x (F ∖ A) z \leftrightarrow (x F z \land \neg x A z)$
4		pm2.27	$⊢ (x F y \land x F z) \to (((x F y \land x F z) \to y = z) \to y = z)$
5	4	ad2ant2r	$⊢ ((x F y \land \neg x A y) \land (x F z \land \neg x A z)) \to (((x F y \land x F z) \to y = z) \to y = z)$
6	2 3 5	syl2anb	$⊢ (x (F ∖ A) y \land x (F ∖ A) z) \to (((x F y \land x F z) \to y = z) \to y = z)$
7	6	com12	$⊢ ((x F y \land x F z) \to y = z) \to ((x (F ∖ A) y \land x (F ∖ A) z) \to y = z)$
8	7	alimi	$⊢ \forall z ((x F y \land x F z) \to y = z) \to \forall z ((x (F ∖ A) y \land x (F ∖ A) z) \to y = z)$
9	8	2alimi	$⊢ \forall x \forall y \forall z ((x F y \land x F z) \to y = z) \to \forall x \forall y \forall z ((x (F ∖ A) y \land x (F ∖ A) z) \to y = z)$
10	1 9	anim12i	$⊢ (Rel F \land \forall x \forall y \forall z ((x F y \land x F z) \to y = z)) \to (Rel (F ∖ A) \land \forall x \forall y \forall z ((x (F ∖ A) y \land x (F ∖ A) z) \to y = z))$
11		dffun2	$⊢ Fun F \leftrightarrow (Rel F \land \forall x \forall y \forall z ((x F y \land x F z) \to y = z))$
12		dffun2	$⊢ Fun (F ∖ A) \leftrightarrow (Rel (F ∖ A) \land \forall x \forall y \forall z ((x (F ∖ A) y \land x (F ∖ A) z) \to y = z))$
13	10 11 12	3imtr4i	$⊢ Fun F \to Fun (F ∖ A)$

Metamath Proof Explorer