Metamath Proof Explorer

Theorem fununfun

Description: If the union of classes is a function, the classes itselves are functions. (Contributed by AV, 18-Jul-2019)

Ref Expression
Assertion fununfun ( Fun ( 𝐹 ∪ 𝐺 ) → ( Fun 𝐹 ∧ Fun 𝐺 ) )

Proof

Step Hyp Ref Expression
1 funrel ⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → Rel ( 𝐹 ∪ 𝐺 ) )
2 relun ⊢ ( Rel ( 𝐹 ∪ 𝐺 ) ↔ ( Rel 𝐹 ∧ Rel 𝐺 ) )
3 1 2 sylib ⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → ( Rel 𝐹 ∧ Rel 𝐺 ) )
4 simpl ⊢ ( ( Rel 𝐹 ∧ Rel 𝐺 ) → Rel 𝐹 )
5 fununmo ⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → ∃* 𝑦 𝑥 𝐹 𝑦 )
6 5 alrimiv ⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 )
7 4 6 anim12i ⊢ ( ( ( Rel 𝐹 ∧ Rel 𝐺 ) ∧ Fun ( 𝐹 ∪ 𝐺 ) ) → ( Rel 𝐹 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 ) )
8 dffun6 ⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 ) )
9 7 8 sylibr ⊢ ( ( ( Rel 𝐹 ∧ Rel 𝐺 ) ∧ Fun ( 𝐹 ∪ 𝐺 ) ) → Fun 𝐹 )
10 simpr ⊢ ( ( Rel 𝐹 ∧ Rel 𝐺 ) → Rel 𝐺 )
11 uncom ⊢ ( 𝐹 ∪ 𝐺 ) = ( 𝐺 ∪ 𝐹 )
12 11 funeqi ⊢ ( Fun ( 𝐹 ∪ 𝐺 ) ↔ Fun ( 𝐺 ∪ 𝐹 ) )
13 fununmo ⊢ ( Fun ( 𝐺 ∪ 𝐹 ) → ∃* 𝑦 𝑥 𝐺 𝑦 )
14 12 13 sylbi ⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → ∃* 𝑦 𝑥 𝐺 𝑦 )
15 14 alrimiv ⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → ∀ 𝑥 ∃* 𝑦 𝑥 𝐺 𝑦 )
16 10 15 anim12i ⊢ ( ( ( Rel 𝐹 ∧ Rel 𝐺 ) ∧ Fun ( 𝐹 ∪ 𝐺 ) ) → ( Rel 𝐺 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐺 𝑦 ) )
17 dffun6 ⊢ ( Fun 𝐺 ↔ ( Rel 𝐺 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐺 𝑦 ) )
18 16 17 sylibr ⊢ ( ( ( Rel 𝐹 ∧ Rel 𝐺 ) ∧ Fun ( 𝐹 ∪ 𝐺 ) ) → Fun 𝐺 )
19 9 18 jca ⊢ ( ( ( Rel 𝐹 ∧ Rel 𝐺 ) ∧ Fun ( 𝐹 ∪ 𝐺 ) ) → ( Fun 𝐹 ∧ Fun 𝐺 ) )
20 3 19 mpancom ⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → ( Fun 𝐹 ∧ Fun 𝐺 ) )