Theorem fununfun

Description: If the union of classes is a function, the classes themselves are functions. (Contributed by AV, 18-Jul-2019) Shorten proof and remove dependency on ax-sep and ax-pr . (Revised by Eric Schmidt, 24-Oct-2026)

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

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ 𝐹 ⊆ ( 𝐹 ∪ 𝐺 )
2		funss	⊢ ( 𝐹 ⊆ ( 𝐹 ∪ 𝐺 ) → ( Fun ( 𝐹 ∪ 𝐺 ) → Fun 𝐹 ) )
3	1 2	ax-mp	⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → Fun 𝐹 )
4		ssun2	⊢ 𝐺 ⊆ ( 𝐹 ∪ 𝐺 )
5		funss	⊢ ( 𝐺 ⊆ ( 𝐹 ∪ 𝐺 ) → ( Fun ( 𝐹 ∪ 𝐺 ) → Fun 𝐺 ) )
6	4 5	ax-mp	⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → Fun 𝐺 )
7	3 6	jca	⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → ( Fun 𝐹 ∧ Fun 𝐺 ) )