Metamath Proof Explorer

Theorem uniinqs

Description: Class union distributes over the intersection of two subclasses of a quotient space. Compare uniin . (Contributed by FL, 25-May-2007) (Proof shortened by Mario Carneiro, 11-Jul-2014)

Ref Expression
Hypothesis uniinqs.1 ⊢ 𝑅 Er 𝑋
Assertion uniinqs ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) → ∪ ( 𝐵 ∩ 𝐶 ) = ( ∪ 𝐵 ∩ ∪ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 uniinqs.1 ⊢ 𝑅 Er 𝑋
2 uniin ⊢ ∪ ( 𝐵 ∩ 𝐶 ) ⊆ ( ∪ 𝐵 ∩ ∪ 𝐶 )
3 2 a1i ⊢ ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) → ∪ ( 𝐵 ∩ 𝐶 ) ⊆ ( ∪ 𝐵 ∩ ∪ 𝐶 ) )
4 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐵 ↔ ∃ 𝑏 ∈ 𝐵 𝑥 ∈ 𝑏 )
5 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐶 ↔ ∃ 𝑐 ∈ 𝐶 𝑥 ∈ 𝑐 )
6 4 5 anbi12i ⊢ ( ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑥 ∈ ∪ 𝐶 ) ↔ ( ∃ 𝑏 ∈ 𝐵 𝑥 ∈ 𝑏 ∧ ∃ 𝑐 ∈ 𝐶 𝑥 ∈ 𝑐 ) )
7 elin ⊢ ( 𝑥 ∈ ( ∪ 𝐵 ∩ ∪ 𝐶 ) ↔ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑥 ∈ ∪ 𝐶 ) )
8 reeanv ⊢ ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ↔ ( ∃ 𝑏 ∈ 𝐵 𝑥 ∈ 𝑏 ∧ ∃ 𝑐 ∈ 𝐶 𝑥 ∈ 𝑐 ) )
9 6 7 8 3bitr4i ⊢ ( 𝑥 ∈ ( ∪ 𝐵 ∩ ∪ 𝐶 ) ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) )
10 simp3l ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → 𝑥 ∈ 𝑏 )
11 simp2l ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → 𝑏 ∈ 𝐵 )
12 inelcm ⊢ ( ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) → ( 𝑏 ∩ 𝑐 ) ≠ ∅ )
13 12 3ad2ant3 ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → ( 𝑏 ∩ 𝑐 ) ≠ ∅ )
14 1 a1i ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → 𝑅 Er 𝑋 )
15 simp1l ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → 𝐵 ⊆ ( 𝐴 / 𝑅 ) )
16 15 11 sseldd ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → 𝑏 ∈ ( 𝐴 / 𝑅 ) )
17 simp1r ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → 𝐶 ⊆ ( 𝐴 / 𝑅 ) )
18 simp2r ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → 𝑐 ∈ 𝐶 )
19 17 18 sseldd ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → 𝑐 ∈ ( 𝐴 / 𝑅 ) )
20 14 16 19 qsdisj ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → ( 𝑏 = 𝑐 ∨ ( 𝑏 ∩ 𝑐 ) = ∅ ) )
21 20 ord ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → ( ¬ 𝑏 = 𝑐 → ( 𝑏 ∩ 𝑐 ) = ∅ ) )
22 21 necon1ad ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → ( ( 𝑏 ∩ 𝑐 ) ≠ ∅ → 𝑏 = 𝑐 ) )
23 13 22 mpd ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → 𝑏 = 𝑐 )
24 23 18 eqeltrd ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → 𝑏 ∈ 𝐶 )
25 11 24 elind ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → 𝑏 ∈ ( 𝐵 ∩ 𝐶 ) )
26 elunii ⊢ ( ( 𝑥 ∈ 𝑏 ∧ 𝑏 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 ∈ ∪ ( 𝐵 ∩ 𝐶 ) )
27 10 25 26 syl2anc ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) ) → 𝑥 ∈ ∪ ( 𝐵 ∩ 𝐶 ) )
28 27 3expia ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) → 𝑥 ∈ ∪ ( 𝐵 ∩ 𝐶 ) ) )
29 28 rexlimdvva ⊢ ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ( 𝑥 ∈ 𝑏 ∧ 𝑥 ∈ 𝑐 ) → 𝑥 ∈ ∪ ( 𝐵 ∩ 𝐶 ) ) )
30 9 29 syl5bi ⊢ ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) → ( 𝑥 ∈ ( ∪ 𝐵 ∩ ∪ 𝐶 ) → 𝑥 ∈ ∪ ( 𝐵 ∩ 𝐶 ) ) )
31 30 ssrdv ⊢ ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) → ( ∪ 𝐵 ∩ ∪ 𝐶 ) ⊆ ∪ ( 𝐵 ∩ 𝐶 ) )
32 3 31 eqssd ⊢ ( ( 𝐵 ⊆ ( 𝐴 / 𝑅 ) ∧ 𝐶 ⊆ ( 𝐴 / 𝑅 ) ) → ∪ ( 𝐵 ∩ 𝐶 ) = ( ∪ 𝐵 ∩ ∪ 𝐶 ) )