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	$⊢ E = Slot N$
	Assertion	strfvss	$⊢ E (S) \subseteq ⋃ ran S$

Proof

Step	Hyp	Ref	Expression
1		strfvss.e	$⊢ E = Slot N$
2		id	$⊢ S \in V \to S \in V$
3	1 2	strfvnd	$⊢ S \in V \to E (S) = S (N)$
4		fvssunirn	$⊢ S (N) \subseteq ⋃ ran S$
5	3 4	eqsstrdi	$⊢ S \in V \to E (S) \subseteq ⋃ ran S$
6		fvprc	$⊢ \neg S \in V \to E (S) = \emptyset$
7		0ss	$⊢ \emptyset \subseteq ⋃ ran S$
8	6 7	eqsstrdi	$⊢ \neg S \in V \to E (S) \subseteq ⋃ ran S$
9	5 8	pm2.61i	$⊢ E (S) \subseteq ⋃ ran S$