Theorem f1oun

Description: The union of two one-to-one onto functions with disjoint domains and ranges. (Contributed by NM, 26-Mar-1998)

	Ref	Expression
Assertion	f1oun	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1-onto→ ( 𝐵 ∪ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		dff1o4	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 Fn 𝐵 ) )
2		dff1o4	⊢ ( 𝐺 : 𝐶 –1-1-onto→ 𝐷 ↔ ( 𝐺 Fn 𝐶 ∧ ◡ 𝐺 Fn 𝐷 ) )
3		fnun	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐶 ) )
4	3	ex	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶 ) → ( ( 𝐴 ∩ 𝐶 ) = ∅ → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐶 ) ) )
5		fnun	⊢ ( ( ( ◡ 𝐹 Fn 𝐵 ∧ ◡ 𝐺 Fn 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( ◡ 𝐹 ∪ ◡ 𝐺 ) Fn ( 𝐵 ∪ 𝐷 ) )
6		cnvun	⊢ ◡ ( 𝐹 ∪ 𝐺 ) = ( ◡ 𝐹 ∪ ◡ 𝐺 )
7	6	fneq1i	⊢ ( ◡ ( 𝐹 ∪ 𝐺 ) Fn ( 𝐵 ∪ 𝐷 ) ↔ ( ◡ 𝐹 ∪ ◡ 𝐺 ) Fn ( 𝐵 ∪ 𝐷 ) )
8	5 7	sylibr	⊢ ( ( ( ◡ 𝐹 Fn 𝐵 ∧ ◡ 𝐺 Fn 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ◡ ( 𝐹 ∪ 𝐺 ) Fn ( 𝐵 ∪ 𝐷 ) )
9	8	ex	⊢ ( ( ◡ 𝐹 Fn 𝐵 ∧ ◡ 𝐺 Fn 𝐷 ) → ( ( 𝐵 ∩ 𝐷 ) = ∅ → ◡ ( 𝐹 ∪ 𝐺 ) Fn ( 𝐵 ∪ 𝐷 ) ) )
10	4 9	im2anan9	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶 ) ∧ ( ◡ 𝐹 Fn 𝐵 ∧ ◡ 𝐺 Fn 𝐷 ) ) → ( ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐶 ) ∧ ◡ ( 𝐹 ∪ 𝐺 ) Fn ( 𝐵 ∪ 𝐷 ) ) ) )
11	10	an4s	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 Fn 𝐵 ) ∧ ( 𝐺 Fn 𝐶 ∧ ◡ 𝐺 Fn 𝐷 ) ) → ( ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐶 ) ∧ ◡ ( 𝐹 ∪ 𝐺 ) Fn ( 𝐵 ∪ 𝐷 ) ) ) )
12	1 2 11	syl2anb	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ) → ( ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐶 ) ∧ ◡ ( 𝐹 ∪ 𝐺 ) Fn ( 𝐵 ∪ 𝐷 ) ) ) )
13		dff1o4	⊢ ( ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1-onto→ ( 𝐵 ∪ 𝐷 ) ↔ ( ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐶 ) ∧ ◡ ( 𝐹 ∪ 𝐺 ) Fn ( 𝐵 ∪ 𝐷 ) ) )
14	12 13	imbitrrdi	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ) → ( ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1-onto→ ( 𝐵 ∪ 𝐷 ) ) )
15	14	imp	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1-onto→ ( 𝐵 ∪ 𝐷 ) )