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

Metamath Proof Explorer

Theorem restuni3

Proof