Theorem fundif

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

	Ref	Expression
Assertion	fundif	⊢ ( Fun 𝐹 → Fun ( 𝐹 ∖ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		reldif	⊢ ( Rel 𝐹 → Rel ( 𝐹 ∖ 𝐴 ) )
2		brdif	⊢ ( 𝑥 ( 𝐹 ∖ 𝐴 ) 𝑦 ↔ ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 𝐴 𝑦 ) )
3		brdif	⊢ ( 𝑥 ( 𝐹 ∖ 𝐴 ) 𝑧 ↔ ( 𝑥 𝐹 𝑧 ∧ ¬ 𝑥 𝐴 𝑧 ) )
4		pm2.27	⊢ ( ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑧 ) → ( ( ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) → 𝑦 = 𝑧 ) )
5	4	ad2ant2r	⊢ ( ( ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 𝐴 𝑦 ) ∧ ( 𝑥 𝐹 𝑧 ∧ ¬ 𝑥 𝐴 𝑧 ) ) → ( ( ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) → 𝑦 = 𝑧 ) )
6	2 3 5	syl2anb	⊢ ( ( 𝑥 ( 𝐹 ∖ 𝐴 ) 𝑦 ∧ 𝑥 ( 𝐹 ∖ 𝐴 ) 𝑧 ) → ( ( ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) → 𝑦 = 𝑧 ) )
7	6	com12	⊢ ( ( ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) → ( ( 𝑥 ( 𝐹 ∖ 𝐴 ) 𝑦 ∧ 𝑥 ( 𝐹 ∖ 𝐴 ) 𝑧 ) → 𝑦 = 𝑧 ) )
8	7	alimi	⊢ ( ∀ 𝑧 ( ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) → ∀ 𝑧 ( ( 𝑥 ( 𝐹 ∖ 𝐴 ) 𝑦 ∧ 𝑥 ( 𝐹 ∖ 𝐴 ) 𝑧 ) → 𝑦 = 𝑧 ) )
9	8	2alimi	⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝐹 ∖ 𝐴 ) 𝑦 ∧ 𝑥 ( 𝐹 ∖ 𝐴 ) 𝑧 ) → 𝑦 = 𝑧 ) )
10	1 9	anim12i	⊢ ( ( Rel 𝐹 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) ) → ( Rel ( 𝐹 ∖ 𝐴 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝐹 ∖ 𝐴 ) 𝑦 ∧ 𝑥 ( 𝐹 ∖ 𝐴 ) 𝑧 ) → 𝑦 = 𝑧 ) ) )
11		dffun2	⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) ) )
12		dffun2	⊢ ( Fun ( 𝐹 ∖ 𝐴 ) ↔ ( Rel ( 𝐹 ∖ 𝐴 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝐹 ∖ 𝐴 ) 𝑦 ∧ 𝑥 ( 𝐹 ∖ 𝐴 ) 𝑧 ) → 𝑦 = 𝑧 ) ) )
13	10 11 12	3imtr4i	⊢ ( Fun 𝐹 → Fun ( 𝐹 ∖ 𝐴 ) )