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

Metamath Proof Explorer

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 ( 𝐹 ∖ 𝐴 ) )