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