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 F : A 1-1 B G : C 1-1 D A C = B D = F G : A C 1-1 B D

Proof

Step Hyp Ref Expression
1 f1f F : A 1-1 B F : A B
2 1 frnd F : A 1-1 B ran F B
3 f1f G : C 1-1 D G : C D
4 3 frnd G : C 1-1 D ran G D
5 unss12 ran F B ran G D ran F ran G B D
6 2 4 5 syl2an F : A 1-1 B G : C 1-1 D ran F ran G B D
7 f1f1orn F : A 1-1 B F : A 1-1 onto ran F
8 f1f1orn G : C 1-1 D G : C 1-1 onto ran G
9 7 8 anim12i F : A 1-1 B G : C 1-1 D F : A 1-1 onto ran F G : C 1-1 onto ran G
10 simprl F : A 1-1 B G : C 1-1 D A C = B D = A C =
11 ss2in ran F B ran G D ran F ran G B D
12 2 4 11 syl2an F : A 1-1 B G : C 1-1 D ran F ran G B D
13 sseq0 ran F ran G B D B D = ran F ran G =
14 12 13 sylan F : A 1-1 B G : C 1-1 D B D = ran F ran G =
15 14 adantrl F : A 1-1 B G : C 1-1 D A C = B D = ran F ran G =
16 10 15 jca F : A 1-1 B G : C 1-1 D A C = B D = A C = ran F ran G =
17 f1oun F : A 1-1 onto ran F G : C 1-1 onto ran G A C = ran F ran G = F G : A C 1-1 onto ran F ran G
18 9 16 17 syl2an2r F : A 1-1 B G : C 1-1 D A C = B D = F G : A C 1-1 onto ran F ran G
19 f1of1 F G : A C 1-1 onto ran F ran G F G : A C 1-1 ran F ran G
20 18 19 syl F : A 1-1 B G : C 1-1 D A C = B D = F G : A C 1-1 ran F ran G
21 f1ss F G : A C 1-1 ran F ran G ran F ran G B D F G : A C 1-1 B D
22 21 ancoms ran F ran G B D F G : A C 1-1 ran F ran G F G : A C 1-1 B D
23 6 20 22 syl2an2r F : A 1-1 B G : C 1-1 D A C = B D = F G : A C 1-1 B D