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	$⊢ R Er X$
	Assertion	uniinqs	$⊢ (B \subseteq A / R \land C \subseteq A / R) \to ⋃ (B \cap C) = ⋃ B \cap ⋃ C$

Proof

Step	Hyp	Ref	Expression
1		uniinqs.1	$⊢ R Er X$
2		uniin	$⊢ ⋃ (B \cap C) \subseteq ⋃ B \cap ⋃ C$
3	2	a1i	$⊢ (B \subseteq A / R \land C \subseteq A / R) \to ⋃ (B \cap C) \subseteq ⋃ B \cap ⋃ C$
4		eluni2	$⊢ x \in ⋃ B \leftrightarrow \exists b \in B x \in b$
5		eluni2	$⊢ x \in ⋃ C \leftrightarrow \exists c \in C x \in c$
6	4 5	anbi12i	$⊢ (x \in ⋃ B \land x \in ⋃ C) \leftrightarrow (\exists b \in B x \in b \land \exists c \in C x \in c)$
7		elin	$⊢ x \in (⋃ B \cap ⋃ C) \leftrightarrow (x \in ⋃ B \land x \in ⋃ C)$
8		reeanv	$⊢ \exists b \in B \exists c \in C (x \in b \land x \in c) \leftrightarrow (\exists b \in B x \in b \land \exists c \in C x \in c)$
9	6 7 8	3bitr4i	$⊢ x \in (⋃ B \cap ⋃ C) \leftrightarrow \exists b \in B \exists c \in C (x \in b \land x \in c)$
10		simp3l	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to x \in b$
11		simp2l	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to b \in B$
12		inelcm	$⊢ (x \in b \land x \in c) \to b \cap c \neq \emptyset$
13	12	3ad2ant3	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to b \cap c \neq \emptyset$
14	1	a1i	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to R Er X$
15		simp1l	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to B \subseteq A / R$
16	15 11	sseldd	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to b \in (A / R)$
17		simp1r	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to C \subseteq A / R$
18		simp2r	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to c \in C$
19	17 18	sseldd	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to c \in (A / R)$
20	14 16 19	qsdisj	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to (b = c \lor b \cap c = \emptyset)$
21	20	ord	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to (\neg b = c \to b \cap c = \emptyset)$
22	21	necon1ad	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to (b \cap c \neq \emptyset \to b = c)$
23	13 22	mpd	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to b = c$
24	23 18	eqeltrd	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to b \in C$
25	11 24	elind	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to b \in (B \cap C)$
26		elunii	$⊢ (x \in b \land b \in (B \cap C)) \to x \in ⋃ (B \cap C)$
27	10 25 26	syl2anc	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C) \land (x \in b \land x \in c)) \to x \in ⋃ (B \cap C)$
28	27	3expia	$⊢ ((B \subseteq A / R \land C \subseteq A / R) \land (b \in B \land c \in C)) \to ((x \in b \land x \in c) \to x \in ⋃ (B \cap C))$
29	28	rexlimdvva	$⊢ (B \subseteq A / R \land C \subseteq A / R) \to (\exists b \in B \exists c \in C (x \in b \land x \in c) \to x \in ⋃ (B \cap C))$
30	9 29	syl5bi	$⊢ (B \subseteq A / R \land C \subseteq A / R) \to (x \in (⋃ B \cap ⋃ C) \to x \in ⋃ (B \cap C))$
31	30	ssrdv	$⊢ (B \subseteq A / R \land C \subseteq A / R) \to ⋃ B \cap ⋃ C \subseteq ⋃ (B \cap C)$
32	3 31	eqssd	$⊢ (B \subseteq A / R \land C \subseteq A / R) \to ⋃ (B \cap C) = ⋃ B \cap ⋃ C$

Metamath Proof Explorer

Theorem uniinqs

Proof