Theorem refssex

Description: Every set in a refinement has a superset in the original cover. (Contributed by Jeff Hankins, 18-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

	Ref	Expression
Assertion	refssex	$$⊢\left(A\mathrm{Ref}B\wedge S\in A\right)\to \exists x\in BS\subseteq x$$

Proof

Step	Hyp	Ref	Expression
1		refrel	$$⊢\mathrm{Rel}\mathrm{Ref}$$
2	1	brrelex1i	$$⊢A\mathrm{Ref}B\to A\in \mathrm{V}$$
3		eqid	$$⊢\bigcup A=\bigcup A$$
4		eqid	$$⊢\bigcup B=\bigcup B$$
5	3 4	isref	$$⊢A\in \mathrm{V}\to \left(A\mathrm{Ref}B\leftrightarrow \left(\bigcup B=\bigcup A\wedge \forall y\in A\exists x\in By\subseteq x\right)\right)$$
6	5	simplbda	$$⊢\left(A\in \mathrm{V}\wedge A\mathrm{Ref}B\right)\to \forall y\in A\exists x\in By\subseteq x$$
7	2 6	mpancom	$$⊢A\mathrm{Ref}B\to \forall y\in A\exists x\in By\subseteq x$$
8		sseq1	$$⊢y=S\to \left(y\subseteq x\leftrightarrow S\subseteq x\right)$$
9	8	rexbidv	$$⊢y=S\to \left(\exists x\in By\subseteq x\leftrightarrow \exists x\in BS\subseteq x\right)$$
10	9	rspccv	$$⊢\forall y\in A\exists x\in By\subseteq x\to \left(S\in A\to \exists x\in BS\subseteq x\right)$$
11	7 10	syl	$$⊢A\mathrm{Ref}B\to \left(S\in A\to \exists x\in BS\subseteq x\right)$$
12	11	imp	$$⊢\left(A\mathrm{Ref}B\wedge S\in A\right)\to \exists x\in BS\subseteq x$$