Metamath Proof Explorer


Theorem cnrmi

Description: A subspace of a completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion cnrmi ( ( 𝐽 ∈ CNrm ∧ 𝐴𝑉 ) → ( 𝐽t 𝐴 ) ∈ Nrm )

Proof

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 )