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

Metamath Proof Explorer

Theorem f1un

Description: The union of two one-to-one functions with disjoint domains and codomains. (Contributed by BTernaryTau, 3-Dec-2024)

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

Proof

Step Hyp Ref Expression
1 f1f ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 1 frnd ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ran 𝐹 ⊆ 𝐵 )
3 f1f ⊢ ( 𝐺 : 𝐶 –1-1→ 𝐷 → 𝐺 : 𝐶 ⟶ 𝐷 )
4 3 frnd ⊢ ( 𝐺 : 𝐶 –1-1→ 𝐷 → ran 𝐺 ⊆ 𝐷 )
5 unss12 ⊢ ( ( ran 𝐹 ⊆ 𝐵 ∧ ran 𝐺 ⊆ 𝐷 ) → ( ran 𝐹 ∪ ran 𝐺 ) ⊆ ( 𝐵 ∪ 𝐷 ) )
6 2 4 5 syl2an ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) → ( ran 𝐹 ∪ ran 𝐺 ) ⊆ ( 𝐵 ∪ 𝐷 ) )
7 f1f1orn ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
8 f1f1orn ⊢ ( 𝐺 : 𝐶 –1-1→ 𝐷 → 𝐺 : 𝐶 –1-1-onto→ ran 𝐺 )
9 7 8 anim12i ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) → ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ∧ 𝐺 : 𝐶 –1-1-onto→ ran 𝐺 ) )
10 simprl ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( 𝐴 ∩ 𝐶 ) = ∅ )
11 ss2in ⊢ ( ( ran 𝐹 ⊆ 𝐵 ∧ ran 𝐺 ⊆ 𝐷 ) → ( ran 𝐹 ∩ ran 𝐺 ) ⊆ ( 𝐵 ∩ 𝐷 ) )
12 2 4 11 syl2an ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) → ( ran 𝐹 ∩ ran 𝐺 ) ⊆ ( 𝐵 ∩ 𝐷 ) )
13 sseq0 ⊢ ( ( ( ran 𝐹 ∩ ran 𝐺 ) ⊆ ( 𝐵 ∩ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( ran 𝐹 ∩ ran 𝐺 ) = ∅ )
14 12 13 sylan ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( ran 𝐹 ∩ ran 𝐺 ) = ∅ )
15 14 adantrl ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( ran 𝐹 ∩ ran 𝐺 ) = ∅ )
16 10 15 jca ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( ran 𝐹 ∩ ran 𝐺 ) = ∅ ) )
17 f1oun ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ∧ 𝐺 : 𝐶 –1-1-onto→ ran 𝐺 ) ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( ran 𝐹 ∩ ran 𝐺 ) = ∅ ) ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1-onto→ ( ran 𝐹 ∪ ran 𝐺 ) )
18 9 16 17 syl2an2r ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1-onto→ ( ran 𝐹 ∪ ran 𝐺 ) )
19 f1of1 ⊢ ( ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1-onto→ ( ran 𝐹 ∪ ran 𝐺 ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1→ ( ran 𝐹 ∪ ran 𝐺 ) )
20 18 19 syl ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1→ ( ran 𝐹 ∪ ran 𝐺 ) )
21 f1ss ⊢ ( ( ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1→ ( ran 𝐹 ∪ ran 𝐺 ) ∧ ( ran 𝐹 ∪ ran 𝐺 ) ⊆ ( 𝐵 ∪ 𝐷 ) ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1→ ( 𝐵 ∪ 𝐷 ) )
22 21 ancoms ⊢ ( ( ( ran 𝐹 ∪ ran 𝐺 ) ⊆ ( 𝐵 ∪ 𝐷 ) ∧ ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1→ ( ran 𝐹 ∪ ran 𝐺 ) ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1→ ( 𝐵 ∪ 𝐷 ) )
23 6 20 22 syl2an2r ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1→ ( 𝐵 ∪ 𝐷 ) )