Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
2 |
1
|
restin |
⊢ ( ( 𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) = ( 𝐽 ↾t ( 𝐴 ∩ ∪ 𝐽 ) ) ) |
3 |
|
oveq2 |
⊢ ( 𝑥 = ( 𝐴 ∩ ∪ 𝐽 ) → ( 𝐽 ↾t 𝑥 ) = ( 𝐽 ↾t ( 𝐴 ∩ ∪ 𝐽 ) ) ) |
4 |
3
|
eleq1d |
⊢ ( 𝑥 = ( 𝐴 ∩ ∪ 𝐽 ) → ( ( 𝐽 ↾t 𝑥 ) ∈ Nrm ↔ ( 𝐽 ↾t ( 𝐴 ∩ ∪ 𝐽 ) ) ∈ Nrm ) ) |
5 |
1
|
iscnrm |
⊢ ( 𝐽 ∈ CNrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑥 ) ∈ Nrm ) ) |
6 |
5
|
simprbi |
⊢ ( 𝐽 ∈ CNrm → ∀ 𝑥 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑥 ) ∈ Nrm ) |
7 |
6
|
adantr |
⊢ ( ( 𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑥 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑥 ) ∈ Nrm ) |
8 |
|
inss2 |
⊢ ( 𝐴 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽 |
9 |
|
inex1g |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ ∪ 𝐽 ) ∈ V ) |
10 |
|
elpwg |
⊢ ( ( 𝐴 ∩ ∪ 𝐽 ) ∈ V → ( ( 𝐴 ∩ ∪ 𝐽 ) ∈ 𝒫 ∪ 𝐽 ↔ ( 𝐴 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽 ) ) |
11 |
9 10
|
syl |
⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ∩ ∪ 𝐽 ) ∈ 𝒫 ∪ 𝐽 ↔ ( 𝐴 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽 ) ) |
12 |
8 11
|
mpbiri |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ ∪ 𝐽 ) ∈ 𝒫 ∪ 𝐽 ) |
13 |
12
|
adantl |
⊢ ( ( 𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ ∪ 𝐽 ) ∈ 𝒫 ∪ 𝐽 ) |
14 |
4 7 13
|
rspcdva |
⊢ ( ( 𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t ( 𝐴 ∩ ∪ 𝐽 ) ) ∈ Nrm ) |
15 |
2 14
|
eqeltrd |
⊢ ( ( 𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Nrm ) |