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

Metamath Proof Explorer

Theorem fnund

Description: The union of two functions with disjoint domains, a deduction version. (Contributed by metakunt, 28-May-2024)

Ref Expression
Hypotheses fnund.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
fnund.2 ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
fnund.3 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
Assertion fnund ( 𝜑 → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fnund.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2 fnund.2 ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
3 fnund.3 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
4 fnun ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) )
5 1 2 3 4 syl21anc ⊢ ( 𝜑 → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) )