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

Metamath Proof Explorer

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→ ( 𝐵 ∪ 𝐷 ) )