# Metamath Proof Explorer

## Theorem 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 ${⊢}{\phi }\to {A}\in {V}$
restuni3.2 ${⊢}{\phi }\to {B}\in {W}$
Assertion restuni3 ${⊢}{\phi }\to \bigcup \left({A}{↾}_{𝑡}{B}\right)=\bigcup {A}\cap {B}$

### Proof

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