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	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐶 ) ∩ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝐷 ) ) = ∅ )