Metamath Proof Explorer


Theorem restuni2

Description: The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis restin.1 𝑋 = 𝐽
Assertion restuni2 ( ( 𝐽 ∈ Top ∧ 𝐴𝑉 ) → ( 𝐴𝑋 ) = ( 𝐽t 𝐴 ) )

Proof

Step Hyp Ref Expression
1 restin.1 𝑋 = 𝐽
2 simpl ( ( 𝐽 ∈ Top ∧ 𝐴𝑉 ) → 𝐽 ∈ Top )
3 inss2 ( 𝐴𝑋 ) ⊆ 𝑋
4 1 restuni ( ( 𝐽 ∈ Top ∧ ( 𝐴𝑋 ) ⊆ 𝑋 ) → ( 𝐴𝑋 ) = ( 𝐽t ( 𝐴𝑋 ) ) )
5 2 3 4 sylancl ( ( 𝐽 ∈ Top ∧ 𝐴𝑉 ) → ( 𝐴𝑋 ) = ( 𝐽t ( 𝐴𝑋 ) ) )
6 1 restin ( ( 𝐽 ∈ Top ∧ 𝐴𝑉 ) → ( 𝐽t 𝐴 ) = ( 𝐽t ( 𝐴𝑋 ) ) )
7 6 unieqd ( ( 𝐽 ∈ Top ∧ 𝐴𝑉 ) → ( 𝐽t 𝐴 ) = ( 𝐽t ( 𝐴𝑋 ) ) )
8 5 7 eqtr4d ( ( 𝐽 ∈ Top ∧ 𝐴𝑉 ) → ( 𝐴𝑋 ) = ( 𝐽t 𝐴 ) )