This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
restuni3.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion restuni3 ( 𝜑 → ∪ ( 𝐴 ↾t 𝐵 ) = ( ∪ 𝐴 ∩ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 restuni3.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 restuni3.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 eluni2 ⊢ ( 𝑥 ∈ ∪ ( 𝐴 ↾t 𝐵 ) ↔ ∃ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) 𝑥 ∈ 𝑦 )
4 3 biimpi ⊢ ( 𝑥 ∈ ∪ ( 𝐴 ↾t 𝐵 ) → ∃ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) 𝑥 ∈ 𝑦 )
5 4 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝐴 ↾t 𝐵 ) ) → ∃ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) 𝑥 ∈ 𝑦 )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) ) → 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) )
7 elrest ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝑧 ∩ 𝐵 ) ) )
8 1 2 7 syl2anc ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝑧 ∩ 𝐵 ) ) )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) ) → ( 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝑧 ∩ 𝐵 ) ) )
10 6 9 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) ) → ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝑧 ∩ 𝐵 ) )
11 10 3adant3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) ∧ 𝑥 ∈ 𝑦 ) → ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝑧 ∩ 𝐵 ) )
12 simpl ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( 𝑧 ∩ 𝐵 ) ) → 𝑥 ∈ 𝑦 )
13 simpr ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( 𝑧 ∩ 𝐵 ) ) → 𝑦 = ( 𝑧 ∩ 𝐵 ) )
14 12 13 eleqtrd ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( 𝑧 ∩ 𝐵 ) ) → 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) )
15 14 ex ⊢ ( 𝑥 ∈ 𝑦 → ( 𝑦 = ( 𝑧 ∩ 𝐵 ) → 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) ) )
16 15 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝑦 = ( 𝑧 ∩ 𝐵 ) → 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) ) )
17 16 reximdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) ∧ 𝑥 ∈ 𝑦 ) → ( ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝑧 ∩ 𝐵 ) → ∃ 𝑧 ∈ 𝐴 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) ) )
18 11 17 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) ∧ 𝑥 ∈ 𝑦 ) → ∃ 𝑧 ∈ 𝐴 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) )
19 18 3exp ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) → ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) ) ) )
20 19 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝐴 ↾t 𝐵 ) ) → ( ∃ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) ) )
22 5 21 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝐴 ↾t 𝐵 ) ) → ∃ 𝑧 ∈ 𝐴 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) )
23 elinel1 ⊢ ( 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) → 𝑥 ∈ 𝑧 )
24 23 adantl ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) ) → 𝑥 ∈ 𝑧 )
25 simpl ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) ) → 𝑧 ∈ 𝐴 )
26 elunii ⊢ ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) → 𝑥 ∈ ∪ 𝐴 )
27 24 25 26 syl2anc ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) ) → 𝑥 ∈ ∪ 𝐴 )
28 elinel2 ⊢ ( 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) → 𝑥 ∈ 𝐵 )
29 28 adantl ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
30 27 29 elind ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) ) → 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) )
31 30 ex ⊢ ( 𝑧 ∈ 𝐴 → ( 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) → 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ) )
32 31 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝐴 ↾t 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) → 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ) )
33 32 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝐴 ↾t 𝐵 ) ) → ( ∃ 𝑧 ∈ 𝐴 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) → 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ) )
34 22 33 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝐴 ↾t 𝐵 ) ) → 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) )
35 34 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ∪ ( 𝐴 ↾t 𝐵 ) 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) )
36 dfss3 ⊢ ( ∪ ( 𝐴 ↾t 𝐵 ) ⊆ ( ∪ 𝐴 ∩ 𝐵 ) ↔ ∀ 𝑥 ∈ ∪ ( 𝐴 ↾t 𝐵 ) 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) )
37 35 36 sylibr ⊢ ( 𝜑 → ∪ ( 𝐴 ↾t 𝐵 ) ⊆ ( ∪ 𝐴 ∩ 𝐵 ) )
38 elinel1 ⊢ ( 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) → 𝑥 ∈ ∪ 𝐴 )
39 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑧 ∈ 𝐴 𝑥 ∈ 𝑧 )
40 38 39 sylib ⊢ ( 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) → ∃ 𝑧 ∈ 𝐴 𝑥 ∈ 𝑧 )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ) → ∃ 𝑧 ∈ 𝐴 𝑥 ∈ 𝑧 )
42 1 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐴 ∈ 𝑉 )
43 2 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
44 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
45 eqid ⊢ ( 𝑧 ∩ 𝐵 ) = ( 𝑧 ∩ 𝐵 )
46 42 43 44 45 elrestd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∩ 𝐵 ) ∈ ( 𝐴 ↾t 𝐵 ) )
47 46 3adant3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝑧 ) → ( 𝑧 ∩ 𝐵 ) ∈ ( 𝐴 ↾t 𝐵 ) )
48 47 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝑧 ) → ( 𝑧 ∩ 𝐵 ) ∈ ( 𝐴 ↾t 𝐵 ) )
49 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 )
50 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) )
51 elinel2 ⊢ ( 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) → 𝑥 ∈ 𝐵 )
52 50 51 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ 𝐵 )
53 simpl ⊢ ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝑧 )
54 simpr ⊢ ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
55 53 54 elind ⊢ ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) )
56 49 52 55 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) )
57 eleq2 ⊢ ( 𝑦 = ( 𝑧 ∩ 𝐵 ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) ) )
58 57 rspcev ⊢ ( ( ( 𝑧 ∩ 𝐵 ) ∈ ( 𝐴 ↾t 𝐵 ) ∧ 𝑥 ∈ ( 𝑧 ∩ 𝐵 ) ) → ∃ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) 𝑥 ∈ 𝑦 )
59 48 56 58 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝑧 ) → ∃ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) 𝑥 ∈ 𝑦 )
60 59 3exp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ) → ( 𝑧 ∈ 𝐴 → ( 𝑥 ∈ 𝑧 → ∃ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) 𝑥 ∈ 𝑦 ) ) )
61 60 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ) → ( ∃ 𝑧 ∈ 𝐴 𝑥 ∈ 𝑧 → ∃ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) 𝑥 ∈ 𝑦 ) )
62 41 61 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ) → ∃ 𝑦 ∈ ( 𝐴 ↾t 𝐵 ) 𝑥 ∈ 𝑦 )
63 62 3 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ∪ 𝐴 ∩ 𝐵 ) ) → 𝑥 ∈ ∪ ( 𝐴 ↾t 𝐵 ) )
64 37 63 eqelssd ⊢ ( 𝜑 → ∪ ( 𝐴 ↾t 𝐵 ) = ( ∪ 𝐴 ∩ 𝐵 ) )