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