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	|- ( ( A Ref B /\ S e. A ) -> E. x e. B S C_ x )

Proof

Step	Hyp	Ref	Expression
1		refrel	|- Rel Ref
2	1	brrelex1i	|- ( A Ref B -> A e. _V )
3		eqid	|- U. A = U. A
4		eqid	|- U. B = U. B
5	3 4	isref	|- ( A e. _V -> ( A Ref B <-> ( U. B = U. A /\ A. y e. A E. x e. B y C_ x ) ) )
6	5	simplbda	|- ( ( A e. _V /\ A Ref B ) -> A. y e. A E. x e. B y C_ x )
7	2 6	mpancom	|- ( A Ref B -> A. y e. A E. x e. B y C_ x )
8		sseq1	|- ( y = S -> ( y C_ x <-> S C_ x ) )
9	8	rexbidv	|- ( y = S -> ( E. x e. B y C_ x <-> E. x e. B S C_ x ) )
10	9	rspccv	|- ( A. y e. A E. x e. B y C_ x -> ( S e. A -> E. x e. B S C_ x ) )
11	7 10	syl	|- ( A Ref B -> ( S e. A -> E. x e. B S C_ x ) )
12	11	imp	|- ( ( A Ref B /\ S e. A ) -> E. x e. B S C_ x )