restuni3

Description: The underlying set of a subspace induced by the subspace operator ` |``t ` . The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	restuni3.1	$⊢ φ \to A \in V$
	restuni3.2	$⊢ φ \to B \in W$
Assertion	restuni3	$⊢ φ \to ⋃ (A ↾_{𝑡} B) = ⋃ A \cap B$

Proof

Step	Hyp	Ref	Expression
1		restuni3.1	$⊢ φ \to A \in V$
2		restuni3.2	$⊢ φ \to B \in W$
3		eluni2	$⊢ x \in ⋃ (A ↾_{𝑡} B) \leftrightarrow \exists y \in (A ↾_{𝑡} B) x \in y$
4	3	bilani	$⊢ (φ \land x \in ⋃ (A ↾_{𝑡} B)) \to \exists y \in (A ↾_{𝑡} B) x \in y$
5		simpr	$⊢ (φ \land y \in (A ↾_{𝑡} B)) \to y \in (A ↾_{𝑡} B)$
6		elrest	$⊢ (A \in V \land B \in W) \to (y \in (A ↾_{𝑡} B) \leftrightarrow \exists z \in A y = z \cap B)$
7	1 2 6	syl2anc	$⊢ φ \to (y \in (A ↾_{𝑡} B) \leftrightarrow \exists z \in A y = z \cap B)$
8	7	adantr	$⊢ (φ \land y \in (A ↾_{𝑡} B)) \to (y \in (A ↾_{𝑡} B) \leftrightarrow \exists z \in A y = z \cap B)$
9	5 8	mpbid	$⊢ (φ \land y \in (A ↾_{𝑡} B)) \to \exists z \in A y = z \cap B$
10	9	3adant3	$⊢ (φ \land y \in (A ↾_{𝑡} B) \land x \in y) \to \exists z \in A y = z \cap B$
11		simpl	$⊢ (x \in y \land y = z \cap B) \to x \in y$
12		simpr	$⊢ (x \in y \land y = z \cap B) \to y = z \cap B$
13	11 12	eleqtrd	$⊢ (x \in y \land y = z \cap B) \to x \in (z \cap B)$
14	13	ex	$⊢ x \in y \to (y = z \cap B \to x \in (z \cap B))$
15	14	3ad2ant3	$⊢ (φ \land y \in (A ↾_{𝑡} B) \land x \in y) \to (y = z \cap B \to x \in (z \cap B))$
16	15	reximdv	$⊢ (φ \land y \in (A ↾_{𝑡} B) \land x \in y) \to (\exists z \in A y = z \cap B \to \exists z \in A x \in (z \cap B))$
17	10 16	mpd	$⊢ (φ \land y \in (A ↾_{𝑡} B) \land x \in y) \to \exists z \in A x \in (z \cap B)$
18	17	3exp	$⊢ φ \to (y \in (A ↾_{𝑡} B) \to (x \in y \to \exists z \in A x \in (z \cap B)))$
19	18	rexlimdv	$⊢ φ \to (\exists y \in (A ↾_{𝑡} B) x \in y \to \exists z \in A x \in (z \cap B))$
20	19	adantr	$⊢ (φ \land x \in ⋃ (A ↾_{𝑡} B)) \to (\exists y \in (A ↾_{𝑡} B) x \in y \to \exists z \in A x \in (z \cap B))$
21	4 20	mpd	$⊢ (φ \land x \in ⋃ (A ↾_{𝑡} B)) \to \exists z \in A x \in (z \cap B)$
22		elinel1	$⊢ x \in (z \cap B) \to x \in z$
23	22	adantl	$⊢ (z \in A \land x \in (z \cap B)) \to x \in z$
24		simpl	$⊢ (z \in A \land x \in (z \cap B)) \to z \in A$
25		elunii	$⊢ (x \in z \land z \in A) \to x \in ⋃ A$
26	23 24 25	syl2anc	$⊢ (z \in A \land x \in (z \cap B)) \to x \in ⋃ A$
27		elinel2	$⊢ x \in (z \cap B) \to x \in B$
28	27	adantl	$⊢ (z \in A \land x \in (z \cap B)) \to x \in B$
29	26 28	elind	$⊢ (z \in A \land x \in (z \cap B)) \to x \in (⋃ A \cap B)$
30	29	ex	$⊢ z \in A \to (x \in (z \cap B) \to x \in (⋃ A \cap B))$
31	30	adantl	$⊢ ((φ \land x \in ⋃ (A ↾_{𝑡} B)) \land z \in A) \to (x \in (z \cap B) \to x \in (⋃ A \cap B))$
32	31	rexlimdva	$⊢ (φ \land x \in ⋃ (A ↾_{𝑡} B)) \to (\exists z \in A x \in (z \cap B) \to x \in (⋃ A \cap B))$
33	21 32	mpd	$⊢ (φ \land x \in ⋃ (A ↾_{𝑡} B)) \to x \in (⋃ A \cap B)$
34	33	ralrimiva	$⊢ φ \to \forall x \in ⋃ (A ↾_{𝑡} B) x \in (⋃ A \cap B)$
35		dfss3	$⊢ ⋃ (A ↾_{𝑡} B) \subseteq ⋃ A \cap B \leftrightarrow \forall x \in ⋃ (A ↾_{𝑡} B) x \in (⋃ A \cap B)$
36	34 35	sylibr	$⊢ φ \to ⋃ (A ↾_{𝑡} B) \subseteq ⋃ A \cap B$
37		elinel1	$⊢ x \in (⋃ A \cap B) \to x \in ⋃ A$
38		eluni2	$⊢ x \in ⋃ A \leftrightarrow \exists z \in A x \in z$
39	37 38	sylib	$⊢ x \in (⋃ A \cap B) \to \exists z \in A x \in z$
40	39	adantl	$⊢ (φ \land x \in (⋃ A \cap B)) \to \exists z \in A x \in z$
41	1	adantr	$⊢ (φ \land z \in A) \to A \in V$
42	2	adantr	$⊢ (φ \land z \in A) \to B \in W$
43		simpr	$⊢ (φ \land z \in A) \to z \in A$
44		eqid	$⊢ z \cap B = z \cap B$
45	41 42 43 44	elrestd	$⊢ (φ \land z \in A) \to z \cap B \in (A ↾_{𝑡} B)$
46	45	3adant3	$⊢ (φ \land z \in A \land x \in z) \to z \cap B \in (A ↾_{𝑡} B)$
47	46	3adant1r	$⊢ ((φ \land x \in (⋃ A \cap B)) \land z \in A \land x \in z) \to z \cap B \in (A ↾_{𝑡} B)$
48		simp3	$⊢ ((φ \land x \in (⋃ A \cap B)) \land z \in A \land x \in z) \to x \in z$
49		simp1r	$⊢ ((φ \land x \in (⋃ A \cap B)) \land z \in A \land x \in z) \to x \in (⋃ A \cap B)$
50		elinel2	$⊢ x \in (⋃ A \cap B) \to x \in B$
51	49 50	syl	$⊢ ((φ \land x \in (⋃ A \cap B)) \land z \in A \land x \in z) \to x \in B$
52		simpl	$⊢ (x \in z \land x \in B) \to x \in z$
53		simpr	$⊢ (x \in z \land x \in B) \to x \in B$
54	52 53	elind	$⊢ (x \in z \land x \in B) \to x \in (z \cap B)$
55	48 51 54	syl2anc	$⊢ ((φ \land x \in (⋃ A \cap B)) \land z \in A \land x \in z) \to x \in (z \cap B)$
56		eleq2	$⊢ y = z \cap B \to (x \in y \leftrightarrow x \in (z \cap B))$
57	56	rspcev	$⊢ (z \cap B \in (A ↾_{𝑡} B) \land x \in (z \cap B)) \to \exists y \in (A ↾_{𝑡} B) x \in y$
58	47 55 57	syl2anc	$⊢ ((φ \land x \in (⋃ A \cap B)) \land z \in A \land x \in z) \to \exists y \in (A ↾_{𝑡} B) x \in y$
59	58	3exp	$⊢ (φ \land x \in (⋃ A \cap B)) \to (z \in A \to (x \in z \to \exists y \in (A ↾_{𝑡} B) x \in y))$
60	59	rexlimdv	$⊢ (φ \land x \in (⋃ A \cap B)) \to (\exists z \in A x \in z \to \exists y \in (A ↾_{𝑡} B) x \in y)$
61	40 60	mpd	$⊢ (φ \land x \in (⋃ A \cap B)) \to \exists y \in (A ↾_{𝑡} B) x \in y$
62	61 3	sylibr	$⊢ (φ \land x \in (⋃ A \cap B)) \to x \in ⋃ (A ↾_{𝑡} B)$
63	36 62	eqelssd	$⊢ φ \to ⋃ (A ↾_{𝑡} B) = ⋃ A \cap B$

Metamath Proof Explorer

Theorem restuni3

Proof