Theorem sess1

Description: Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015)

	Ref	Expression
Assertion	sess1	$$⊢R\subseteq S\to \left(S\mathrm{Se}A\to R\mathrm{Se}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(R\subseteq S\wedge y\in A\right)\to R\subseteq S$$
2	1	ssbrd	$$⊢\left(R\subseteq S\wedge y\in A\right)\to \left(yRx\to ySx\right)$$
3	2	ss2rabdv	$$⊢R\subseteq S\to \left\{y\in A|yRx\right\}\subseteq \left\{y\in A|ySx\right\}$$
4		ssexg	$$⊢\left(\left\{y\in A|yRx\right\}\subseteq \left\{y\in A|ySx\right\}\wedge \left\{y\in A|ySx\right\}\in \mathrm{V}\right)\to \left\{y\in A|yRx\right\}\in \mathrm{V}$$
5	4	ex	$$⊢\left\{y\in A|yRx\right\}\subseteq \left\{y\in A|ySx\right\}\to \left(\left\{y\in A|ySx\right\}\in \mathrm{V}\to \left\{y\in A|yRx\right\}\in \mathrm{V}\right)$$
6	3 5	syl	$$⊢R\subseteq S\to \left(\left\{y\in A|ySx\right\}\in \mathrm{V}\to \left\{y\in A|yRx\right\}\in \mathrm{V}\right)$$
7	6	ralimdv	$$⊢R\subseteq S\to \left(\forall x\in A\left\{y\in A|ySx\right\}\in \mathrm{V}\to \forall x\in A\left\{y\in A|yRx\right\}\in \mathrm{V}\right)$$
8		df-se	$$⊢S\mathrm{Se}A\leftrightarrow \forall x\in A\left\{y\in A|ySx\right\}\in \mathrm{V}$$
9		df-se	$$⊢R\mathrm{Se}A\leftrightarrow \forall x\in A\left\{y\in A|yRx\right\}\in \mathrm{V}$$
10	7 8 9	3imtr4g	$$⊢R\subseteq S\to \left(S\mathrm{Se}A\to R\mathrm{Se}A\right)$$