Metamath Proof Explorer


Theorem restin

Description: When the subspace region is not a subset of the base of the topology, the resulting set is the same as the subspace restricted to the base. (Contributed by Mario Carneiro, 15-Dec-2013)

Ref Expression
Hypothesis restin.1 𝑋 = 𝐽
Assertion restin ( ( 𝐽𝑉𝐴𝑊 ) → ( 𝐽t 𝐴 ) = ( 𝐽t ( 𝐴𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 restin.1 𝑋 = 𝐽
2 uniexg ( 𝐽𝑉 𝐽 ∈ V )
3 1 2 eqeltrid ( 𝐽𝑉𝑋 ∈ V )
4 3 adantr ( ( 𝐽𝑉𝐴𝑊 ) → 𝑋 ∈ V )
5 restco ( ( 𝐽𝑉𝑋 ∈ V ∧ 𝐴𝑊 ) → ( ( 𝐽t 𝑋 ) ↾t 𝐴 ) = ( 𝐽t ( 𝑋𝐴 ) ) )
6 5 3com23 ( ( 𝐽𝑉𝐴𝑊𝑋 ∈ V ) → ( ( 𝐽t 𝑋 ) ↾t 𝐴 ) = ( 𝐽t ( 𝑋𝐴 ) ) )
7 4 6 mpd3an3 ( ( 𝐽𝑉𝐴𝑊 ) → ( ( 𝐽t 𝑋 ) ↾t 𝐴 ) = ( 𝐽t ( 𝑋𝐴 ) ) )
8 1 restid ( 𝐽𝑉 → ( 𝐽t 𝑋 ) = 𝐽 )
9 8 adantr ( ( 𝐽𝑉𝐴𝑊 ) → ( 𝐽t 𝑋 ) = 𝐽 )
10 9 oveq1d ( ( 𝐽𝑉𝐴𝑊 ) → ( ( 𝐽t 𝑋 ) ↾t 𝐴 ) = ( 𝐽t 𝐴 ) )
11 incom ( 𝑋𝐴 ) = ( 𝐴𝑋 )
12 11 oveq2i ( 𝐽t ( 𝑋𝐴 ) ) = ( 𝐽t ( 𝐴𝑋 ) )
13 12 a1i ( ( 𝐽𝑉𝐴𝑊 ) → ( 𝐽t ( 𝑋𝐴 ) ) = ( 𝐽t ( 𝐴𝑋 ) ) )
14 7 10 13 3eqtr3d ( ( 𝐽𝑉𝐴𝑊 ) → ( 𝐽t 𝐴 ) = ( 𝐽t ( 𝐴𝑋 ) ) )