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

Metamath Proof Explorer

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 )