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

Metamath Proof Explorer

Theorem strfvss

Description: A structure component extractor produces a value which is contained in a set dependent on S , but not E . This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015)

Ref Expression
Hypothesis strfvss.e ⊢ 𝐸 = Slot 𝑁
Assertion strfvss ( 𝐸 ‘ 𝑆 ) ⊆ ∪ ran 𝑆

Proof

Step Hyp Ref Expression
1 strfvss.e ⊢ 𝐸 = Slot 𝑁
2 id ⊢ ( 𝑆 ∈ V → 𝑆 ∈ V )
3 1 2 strfvnd ⊢ ( 𝑆 ∈ V → ( 𝐸 ‘ 𝑆 ) = ( 𝑆 ‘ 𝑁 ) )
4 fvssunirn ⊢ ( 𝑆 ‘ 𝑁 ) ⊆ ∪ ran 𝑆
5 3 4 eqsstrdi ⊢ ( 𝑆 ∈ V → ( 𝐸 ‘ 𝑆 ) ⊆ ∪ ran 𝑆 )
6 fvprc ⊢ ( ¬ 𝑆 ∈ V → ( 𝐸 ‘ 𝑆 ) = ∅ )
7 0ss ⊢ ∅ ⊆ ∪ ran 𝑆
8 6 7 eqsstrdi ⊢ ( ¬ 𝑆 ∈ V → ( 𝐸 ‘ 𝑆 ) ⊆ ∪ ran 𝑆 )
9 5 8 pm2.61i ⊢ ( 𝐸 ‘ 𝑆 ) ⊆ ∪ ran 𝑆