This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem strss

Description: Propagate component extraction to a structure T from a subset structure S . (Contributed by Mario Carneiro, 11-Oct-2013) (Revised by Mario Carneiro, 15-Jan-2014)

Ref Expression
Hypotheses strss.t ⊢ 𝑇 ∈ V
strss.f ⊢ Fun 𝑇
strss.s ⊢ 𝑆 ⊆ 𝑇
strss.e ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
strss.n ⊢ ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆
Assertion strss ( 𝐸 ‘ 𝑇 ) = ( 𝐸 ‘ 𝑆 )

Proof

Step Hyp Ref Expression
1 strss.t ⊢ 𝑇 ∈ V
2 strss.f ⊢ Fun 𝑇
3 strss.s ⊢ 𝑆 ⊆ 𝑇
4 strss.e ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
5 strss.n ⊢ ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆
6 1 a1i ⊢ ( ⊤ → 𝑇 ∈ V )
7 2 a1i ⊢ ( ⊤ → Fun 𝑇 )
8 3 a1i ⊢ ( ⊤ → 𝑆 ⊆ 𝑇 )
9 5 a1i ⊢ ( ⊤ → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆 )
10 4 6 7 8 9 strssd ⊢ ( ⊤ → ( 𝐸 ‘ 𝑇 ) = ( 𝐸 ‘ 𝑆 ) )
11 10 mptru ⊢ ( 𝐸 ‘ 𝑇 ) = ( 𝐸 ‘ 𝑆 )