bj-restuni

Description: The union of an elementwise intersection by a set is equal to the intersection with that set of the union of the family. See also restuni and restuni2 . (Contributed by BJ, 27-Apr-2021)

		Ref	Expression
	Assertion	bj-restuni	$⊢ (X \in V \land A \in W) \to ⋃ (X ↾_{𝑡} A) = ⋃ X \cap A$

Proof

Step	Hyp	Ref	Expression
1		eluni	$⊢ x \in ⋃ (X ↾_{𝑡} A) \leftrightarrow \exists y (x \in y \land y \in (X ↾_{𝑡} A))$
2		elrest	$⊢ (X \in V \land A \in W) \to (y \in (X ↾_{𝑡} A) \leftrightarrow \exists z \in X y = z \cap A)$
3	2	anbi2d	$⊢ (X \in V \land A \in W) \to ((x \in y \land y \in (X ↾_{𝑡} A)) \leftrightarrow (x \in y \land \exists z \in X y = z \cap A))$
4	3	exbidv	$⊢ (X \in V \land A \in W) \to (\exists y (x \in y \land y \in (X ↾_{𝑡} A)) \leftrightarrow \exists y (x \in y \land \exists z \in X y = z \cap A))$
5		eluni	$⊢ x \in ⋃ X \leftrightarrow \exists z (x \in z \land z \in X)$
6	5	bicomi	$⊢ \exists z (x \in z \land z \in X) \leftrightarrow x \in ⋃ X$
7	6	anbi1i	$⊢ (\exists z (x \in z \land z \in X) \land x \in A) \leftrightarrow (x \in ⋃ X \land x \in A)$
8	7	a1i	$⊢ (X \in V \land A \in W) \to ((\exists z (x \in z \land z \in X) \land x \in A) \leftrightarrow (x \in ⋃ X \land x \in A))$
9		df-rex	$⊢ \exists z \in X y = z \cap A \leftrightarrow \exists z (z \in X \land y = z \cap A)$
10	9	anbi2i	$⊢ (x \in y \land \exists z \in X y = z \cap A) \leftrightarrow (x \in y \land \exists z (z \in X \land y = z \cap A))$
11		19.42v	$⊢ \exists z (x \in y \land (z \in X \land y = z \cap A)) \leftrightarrow (x \in y \land \exists z (z \in X \land y = z \cap A))$
12	11	bicomi	$⊢ (x \in y \land \exists z (z \in X \land y = z \cap A)) \leftrightarrow \exists z (x \in y \land (z \in X \land y = z \cap A))$
13	10 12	bitri	$⊢ (x \in y \land \exists z \in X y = z \cap A) \leftrightarrow \exists z (x \in y \land (z \in X \land y = z \cap A))$
14	13	exbii	$⊢ \exists y (x \in y \land \exists z \in X y = z \cap A) \leftrightarrow \exists y \exists z (x \in y \land (z \in X \land y = z \cap A))$
15		excom	$⊢ \exists y \exists z (x \in y \land (z \in X \land y = z \cap A)) \leftrightarrow \exists z \exists y (x \in y \land (z \in X \land y = z \cap A))$
16		an12	$⊢ (x \in y \land (z \in X \land y = z \cap A)) \leftrightarrow (z \in X \land (x \in y \land y = z \cap A))$
17	16	exbii	$⊢ \exists y (x \in y \land (z \in X \land y = z \cap A)) \leftrightarrow \exists y (z \in X \land (x \in y \land y = z \cap A))$
18		19.42v	$⊢ \exists y (z \in X \land (x \in y \land y = z \cap A)) \leftrightarrow (z \in X \land \exists y (x \in y \land y = z \cap A))$
19		eqimss	$⊢ y = z \cap A \to y \subseteq z \cap A$
20	19	sseld	$⊢ y = z \cap A \to (x \in y \to x \in (z \cap A))$
21	20	imdistanri	$⊢ (x \in y \land y = z \cap A) \to (x \in (z \cap A) \land y = z \cap A)$
22		eqimss2	$⊢ y = z \cap A \to z \cap A \subseteq y$
23	22	sseld	$⊢ y = z \cap A \to (x \in (z \cap A) \to x \in y)$
24	23	imdistanri	$⊢ (x \in (z \cap A) \land y = z \cap A) \to (x \in y \land y = z \cap A)$
25	21 24	impbii	$⊢ (x \in y \land y = z \cap A) \leftrightarrow (x \in (z \cap A) \land y = z \cap A)$
26	25	exbii	$⊢ \exists y (x \in y \land y = z \cap A) \leftrightarrow \exists y (x \in (z \cap A) \land y = z \cap A)$
27		19.42v	$⊢ \exists y (x \in (z \cap A) \land y = z \cap A) \leftrightarrow (x \in (z \cap A) \land \exists y y = z \cap A)$
28		vex	$⊢ z \in V$
29	28	inex1	$⊢ z \cap A \in V$
30	29	isseti	$⊢ \exists y y = z \cap A$
31	30	biantru	$⊢ x \in (z \cap A) \leftrightarrow (x \in (z \cap A) \land \exists y y = z \cap A)$
32	31	bicomi	$⊢ (x \in (z \cap A) \land \exists y y = z \cap A) \leftrightarrow x \in (z \cap A)$
33		elin	$⊢ x \in (z \cap A) \leftrightarrow (x \in z \land x \in A)$
34	32 33	bitri	$⊢ (x \in (z \cap A) \land \exists y y = z \cap A) \leftrightarrow (x \in z \land x \in A)$
35	26 27 34	3bitri	$⊢ \exists y (x \in y \land y = z \cap A) \leftrightarrow (x \in z \land x \in A)$
36	35	bianassc	$⊢ (z \in X \land \exists y (x \in y \land y = z \cap A)) \leftrightarrow ((x \in z \land z \in X) \land x \in A)$
37	17 18 36	3bitri	$⊢ \exists y (x \in y \land (z \in X \land y = z \cap A)) \leftrightarrow ((x \in z \land z \in X) \land x \in A)$
38	37	exbii	$⊢ \exists z \exists y (x \in y \land (z \in X \land y = z \cap A)) \leftrightarrow \exists z ((x \in z \land z \in X) \land x \in A)$
39		19.41v	$⊢ \exists z ((x \in z \land z \in X) \land x \in A) \leftrightarrow (\exists z (x \in z \land z \in X) \land x \in A)$
40	38 39	bitri	$⊢ \exists z \exists y (x \in y \land (z \in X \land y = z \cap A)) \leftrightarrow (\exists z (x \in z \land z \in X) \land x \in A)$
41	14 15 40	3bitri	$⊢ \exists y (x \in y \land \exists z \in X y = z \cap A) \leftrightarrow (\exists z (x \in z \land z \in X) \land x \in A)$
42		elin	$⊢ x \in (⋃ X \cap A) \leftrightarrow (x \in ⋃ X \land x \in A)$
43	8 41 42	3bitr4g	$⊢ (X \in V \land A \in W) \to (\exists y (x \in y \land \exists z \in X y = z \cap A) \leftrightarrow x \in (⋃ X \cap A))$
44	4 43	bitrd	$⊢ (X \in V \land A \in W) \to (\exists y (x \in y \land y \in (X ↾_{𝑡} A)) \leftrightarrow x \in (⋃ X \cap A))$
45	1 44	syl5bb	$⊢ (X \in V \land A \in W) \to (x \in ⋃ (X ↾_{𝑡} A) \leftrightarrow x \in (⋃ X \cap A))$
46	45	eqrdv	$⊢ (X \in V \land A \in W) \to ⋃ (X ↾_{𝑡} A) = ⋃ X \cap A$

Metamath Proof Explorer

Theorem bj-restuni

Proof