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

Metamath Proof Explorer

Theorem djudisj

Description: Disjoint unions with disjoint index sets are disjoint. (Contributed by Stefan O'Rear, 21-Nov-2014)

Ref Expression
Assertion djudisj ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐶 ) ∩ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝐷 ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 djussxp ⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐶 ) ⊆ ( 𝐴 × V )
2 incom ⊢ ( ( 𝐴 × V ) ∩ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝐷 ) ) = ( ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝐷 ) ∩ ( 𝐴 × V ) )
3 djussxp ⊢ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝐷 ) ⊆ ( 𝐵 × V )
4 incom ⊢ ( ( 𝐵 × V ) ∩ ( 𝐴 × V ) ) = ( ( 𝐴 × V ) ∩ ( 𝐵 × V ) )
5 xpdisj1 ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 × V ) ∩ ( 𝐵 × V ) ) = ∅ )
6 4 5 eqtrid ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐵 × V ) ∩ ( 𝐴 × V ) ) = ∅ )
7 ssdisj ⊢ ( ( ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝐷 ) ⊆ ( 𝐵 × V ) ∧ ( ( 𝐵 × V ) ∩ ( 𝐴 × V ) ) = ∅ ) → ( ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝐷 ) ∩ ( 𝐴 × V ) ) = ∅ )
8 3 6 7 sylancr ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝐷 ) ∩ ( 𝐴 × V ) ) = ∅ )
9 2 8 eqtrid ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 × V ) ∩ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝐷 ) ) = ∅ )
10 ssdisj ⊢ ( ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐶 ) ⊆ ( 𝐴 × V ) ∧ ( ( 𝐴 × V ) ∩ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝐷 ) ) = ∅ ) → ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐶 ) ∩ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝐷 ) ) = ∅ )
11 1 9 10 sylancr ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐶 ) ∩ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝐷 ) ) = ∅ )