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 ⊢ ( 𝜑 → 𝐺 : 𝐴 –1-1-onto→ 𝑋 )
metakunt17.2 ⊢ ( 𝜑 → 𝐻 : 𝐵 –1-1-onto→ 𝑌 )
metakunt17.3 ⊢ ( 𝜑 → 𝐼 : 𝐶 –1-1-onto→ 𝑍 )
metakunt17.4 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
metakunt17.5 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐶 ) = ∅ )
metakunt17.6 ⊢ ( 𝜑 → ( 𝐵 ∩ 𝐶 ) = ∅ )
metakunt17.7 ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) = ∅ )
metakunt17.8 ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑍 ) = ∅ )
metakunt17.9 ⊢ ( 𝜑 → ( 𝑌 ∩ 𝑍 ) = ∅ )
metakunt17.10 ⊢ ( 𝜑 → 𝐹 = ( ( 𝐺 ∪ 𝐻 ) ∪ 𝐼 ) )
metakunt17.11 ⊢ ( 𝜑 → 𝐷 = ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
metakunt17.12 ⊢ ( 𝜑 → 𝑊 = ( ( 𝑋 ∪ 𝑌 ) ∪ 𝑍 ) )
Assertion metakunt17 ( 𝜑 → 𝐹 : 𝐷 –1-1-onto→ 𝑊 )

Proof

Step Hyp Ref Expression
1 metakunt17.1 ⊢ ( 𝜑 → 𝐺 : 𝐴 –1-1-onto→ 𝑋 )
2 metakunt17.2 ⊢ ( 𝜑 → 𝐻 : 𝐵 –1-1-onto→ 𝑌 )
3 metakunt17.3 ⊢ ( 𝜑 → 𝐼 : 𝐶 –1-1-onto→ 𝑍 )
4 metakunt17.4 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
5 metakunt17.5 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐶 ) = ∅ )
6 metakunt17.6 ⊢ ( 𝜑 → ( 𝐵 ∩ 𝐶 ) = ∅ )
7 metakunt17.7 ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) = ∅ )
8 metakunt17.8 ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑍 ) = ∅ )
9 metakunt17.9 ⊢ ( 𝜑 → ( 𝑌 ∩ 𝑍 ) = ∅ )
10 metakunt17.10 ⊢ ( 𝜑 → 𝐹 = ( ( 𝐺 ∪ 𝐻 ) ∪ 𝐼 ) )
11 metakunt17.11 ⊢ ( 𝜑 → 𝐷 = ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
12 metakunt17.12 ⊢ ( 𝜑 → 𝑊 = ( ( 𝑋 ∪ 𝑌 ) ∪ 𝑍 ) )
13 4 7 jca ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ ( 𝑋 ∩ 𝑌 ) = ∅ ) )
14 1 2 13 jca31 ⊢ ( 𝜑 → ( ( 𝐺 : 𝐴 –1-1-onto→ 𝑋 ∧ 𝐻 : 𝐵 –1-1-onto→ 𝑌 ) ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ ( 𝑋 ∩ 𝑌 ) = ∅ ) ) )
15 f1oun ⊢ ( ( ( 𝐺 : 𝐴 –1-1-onto→ 𝑋 ∧ 𝐻 : 𝐵 –1-1-onto→ 𝑌 ) ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ ( 𝑋 ∩ 𝑌 ) = ∅ ) ) → ( 𝐺 ∪ 𝐻 ) : ( 𝐴 ∪ 𝐵 ) –1-1-onto→ ( 𝑋 ∪ 𝑌 ) )
16 14 15 syl ⊢ ( 𝜑 → ( 𝐺 ∪ 𝐻 ) : ( 𝐴 ∪ 𝐵 ) –1-1-onto→ ( 𝑋 ∪ 𝑌 ) )
17 indir ⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐶 ) = ( ( 𝐴 ∩ 𝐶 ) ∪ ( 𝐵 ∩ 𝐶 ) )
18 5 6 uneq12d ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐶 ) ∪ ( 𝐵 ∩ 𝐶 ) ) = ( ∅ ∪ ∅ ) )
19 0un ⊢ ( ∅ ∪ ∅ ) = ∅
20 19 a1i ⊢ ( 𝜑 → ( ∅ ∪ ∅ ) = ∅ )
21 18 20 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐶 ) ∪ ( 𝐵 ∩ 𝐶 ) ) = ∅ )
22 17 21 syl5eq ⊢ ( 𝜑 → ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐶 ) = ∅ )
23 indir ⊢ ( ( 𝑋 ∪ 𝑌 ) ∩ 𝑍 ) = ( ( 𝑋 ∩ 𝑍 ) ∪ ( 𝑌 ∩ 𝑍 ) )
24 8 9 uneq12d ⊢ ( 𝜑 → ( ( 𝑋 ∩ 𝑍 ) ∪ ( 𝑌 ∩ 𝑍 ) ) = ( ∅ ∪ ∅ ) )
25 24 20 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 ∩ 𝑍 ) ∪ ( 𝑌 ∩ 𝑍 ) ) = ∅ )
26 23 25 syl5eq ⊢ ( 𝜑 → ( ( 𝑋 ∪ 𝑌 ) ∩ 𝑍 ) = ∅ )
27 22 26 jca ⊢ ( 𝜑 → ( ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐶 ) = ∅ ∧ ( ( 𝑋 ∪ 𝑌 ) ∩ 𝑍 ) = ∅ ) )
28 16 3 27 jca31 ⊢ ( 𝜑 → ( ( ( 𝐺 ∪ 𝐻 ) : ( 𝐴 ∪ 𝐵 ) –1-1-onto→ ( 𝑋 ∪ 𝑌 ) ∧ 𝐼 : 𝐶 –1-1-onto→ 𝑍 ) ∧ ( ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐶 ) = ∅ ∧ ( ( 𝑋 ∪ 𝑌 ) ∩ 𝑍 ) = ∅ ) ) )
29 f1oun ⊢ ( ( ( ( 𝐺 ∪ 𝐻 ) : ( 𝐴 ∪ 𝐵 ) –1-1-onto→ ( 𝑋 ∪ 𝑌 ) ∧ 𝐼 : 𝐶 –1-1-onto→ 𝑍 ) ∧ ( ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐶 ) = ∅ ∧ ( ( 𝑋 ∪ 𝑌 ) ∩ 𝑍 ) = ∅ ) ) → ( ( 𝐺 ∪ 𝐻 ) ∪ 𝐼 ) : ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) –1-1-onto→ ( ( 𝑋 ∪ 𝑌 ) ∪ 𝑍 ) )
30 28 29 syl ⊢ ( 𝜑 → ( ( 𝐺 ∪ 𝐻 ) ∪ 𝐼 ) : ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) –1-1-onto→ ( ( 𝑋 ∪ 𝑌 ) ∪ 𝑍 ) )
31 10 11 12 f1oeq123d ⊢ ( 𝜑 → ( 𝐹 : 𝐷 –1-1-onto→ 𝑊 ↔ ( ( 𝐺 ∪ 𝐻 ) ∪ 𝐼 ) : ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) –1-1-onto→ ( ( 𝑋 ∪ 𝑌 ) ∪ 𝑍 ) ) )
32 30 31 mpbird ⊢ ( 𝜑 → 𝐹 : 𝐷 –1-1-onto→ 𝑊 )