Metamath Proof Explorer

Theorem metakunt17

Description: The union of three disjoint bijections is a bijection. (Contributed by metakunt, 28-May-2024)

Ref Expression
Hypotheses metakunt17.1 
|- ( ph -> G : A -1-1-onto-> X )
metakunt17.2 
|- ( ph -> H : B -1-1-onto-> Y )
metakunt17.3 
|- ( ph -> I : C -1-1-onto-> Z )
metakunt17.4 
|- ( ph -> ( A i^i B ) = (/) )
metakunt17.5 
|- ( ph -> ( A i^i C ) = (/) )
metakunt17.6 
|- ( ph -> ( B i^i C ) = (/) )
metakunt17.7 
|- ( ph -> ( X i^i Y ) = (/) )
metakunt17.8 
|- ( ph -> ( X i^i Z ) = (/) )
metakunt17.9 
|- ( ph -> ( Y i^i Z ) = (/) )
metakunt17.10 
|- ( ph -> F = ( ( G u. H ) u. I ) )
metakunt17.11 
|- ( ph -> D = ( ( A u. B ) u. C ) )
metakunt17.12 
|- ( ph -> W = ( ( X u. Y ) u. Z ) )
Assertion metakunt17 
|- ( ph -> F : D -1-1-onto-> W )

Proof

Step Hyp Ref Expression
1 metakunt17.1 
 |-  ( ph -> G : A -1-1-onto-> X )
2 metakunt17.2 
 |-  ( ph -> H : B -1-1-onto-> Y )
3 metakunt17.3 
 |-  ( ph -> I : C -1-1-onto-> Z )
4 metakunt17.4 
 |-  ( ph -> ( A i^i B ) = (/) )
5 metakunt17.5 
 |-  ( ph -> ( A i^i C ) = (/) )
6 metakunt17.6 
 |-  ( ph -> ( B i^i C ) = (/) )
7 metakunt17.7 
 |-  ( ph -> ( X i^i Y ) = (/) )
8 metakunt17.8 
 |-  ( ph -> ( X i^i Z ) = (/) )
9 metakunt17.9 
 |-  ( ph -> ( Y i^i Z ) = (/) )
10 metakunt17.10 
 |-  ( ph -> F = ( ( G u. H ) u. I ) )
11 metakunt17.11 
 |-  ( ph -> D = ( ( A u. B ) u. C ) )
12 metakunt17.12 
 |-  ( ph -> W = ( ( X u. Y ) u. Z ) )
13 4 7 jca 
 |-  ( ph -> ( ( A i^i B ) = (/) /\ ( X i^i Y ) = (/) ) )
14 1 2 13 jca31 
 |-  ( ph -> ( ( G : A -1-1-onto-> X /\ H : B -1-1-onto-> Y ) /\ ( ( A i^i B ) = (/) /\ ( X i^i Y ) = (/) ) ) )
15 f1oun 
 |-  ( ( ( G : A -1-1-onto-> X /\ H : B -1-1-onto-> Y ) /\ ( ( A i^i B ) = (/) /\ ( X i^i Y ) = (/) ) ) -> ( G u. H ) : ( A u. B ) -1-1-onto-> ( X u. Y ) )
16 14 15 syl 
 |-  ( ph -> ( G u. H ) : ( A u. B ) -1-1-onto-> ( X u. Y ) )
17 indir 
 |-  ( ( A u. B ) i^i C ) = ( ( A i^i C ) u. ( B i^i C ) )
18 5 6 uneq12d 
 |-  ( ph -> ( ( A i^i C ) u. ( B i^i C ) ) = ( (/) u. (/) ) )
19 0un 
 |-  ( (/) u. (/) ) = (/)
20 19 a1i 
 |-  ( ph -> ( (/) u. (/) ) = (/) )
21 18 20 eqtrd 
 |-  ( ph -> ( ( A i^i C ) u. ( B i^i C ) ) = (/) )
22 17 21 syl5eq 
 |-  ( ph -> ( ( A u. B ) i^i C ) = (/) )
23 indir 
 |-  ( ( X u. Y ) i^i Z ) = ( ( X i^i Z ) u. ( Y i^i Z ) )
24 8 9 uneq12d 
 |-  ( ph -> ( ( X i^i Z ) u. ( Y i^i Z ) ) = ( (/) u. (/) ) )
25 24 20 eqtrd 
 |-  ( ph -> ( ( X i^i Z ) u. ( Y i^i Z ) ) = (/) )
26 23 25 syl5eq 
 |-  ( ph -> ( ( X u. Y ) i^i Z ) = (/) )
27 22 26 jca 
 |-  ( ph -> ( ( ( A u. B ) i^i C ) = (/) /\ ( ( X u. Y ) i^i Z ) = (/) ) )
28 16 3 27 jca31 
 |-  ( ph -> ( ( ( G u. H ) : ( A u. B ) -1-1-onto-> ( X u. Y ) /\ I : C -1-1-onto-> Z ) /\ ( ( ( A u. B ) i^i C ) = (/) /\ ( ( X u. Y ) i^i Z ) = (/) ) ) )
29 f1oun 
 |-  ( ( ( ( G u. H ) : ( A u. B ) -1-1-onto-> ( X u. Y ) /\ I : C -1-1-onto-> Z ) /\ ( ( ( A u. B ) i^i C ) = (/) /\ ( ( X u. Y ) i^i Z ) = (/) ) ) -> ( ( G u. H ) u. I ) : ( ( A u. B ) u. C ) -1-1-onto-> ( ( X u. Y ) u. Z ) )
30 28 29 syl 
 |-  ( ph -> ( ( G u. H ) u. I ) : ( ( A u. B ) u. C ) -1-1-onto-> ( ( X u. Y ) u. Z ) )
31 10 11 12 f1oeq123d 
 |-  ( ph -> ( F : D -1-1-onto-> W <-> ( ( G u. H ) u. I ) : ( ( A u. B ) u. C ) -1-1-onto-> ( ( X u. Y ) u. Z ) ) )
32 30 31 mpbird 
 |-  ( ph -> F : D -1-1-onto-> W )