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

Metamath Proof Explorer

Theorem ssref

Description: A subcover is a refinement of the original cover. (Contributed by Jeff Hankins, 18-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

Ref Expression
Hypotheses ssref.1 
|- X = U. A
ssref.2 
|- Y = U. B
Assertion ssref 
|- ( ( A e. C /\ A C_ B /\ X = Y ) -> A Ref B )

Proof

Step Hyp Ref Expression
1 ssref.1 
 |-  X = U. A
2 ssref.2 
 |-  Y = U. B
3 eqcom 
 |-  ( X = Y <-> Y = X )
4 3 biimpi 
 |-  ( X = Y -> Y = X )
5 4 3ad2ant3 
 |-  ( ( A e. C /\ A C_ B /\ X = Y ) -> Y = X )
6 ssel2 
 |-  ( ( A C_ B /\ x e. A ) -> x e. B )
7 6 3ad2antl2 
 |-  ( ( ( A e. C /\ A C_ B /\ X = Y ) /\ x e. A ) -> x e. B )
8 ssid 
 |-  x C_ x
9 sseq2 
 |-  ( y = x -> ( x C_ y <-> x C_ x ) )
10 9 rspcev 
 |-  ( ( x e. B /\ x C_ x ) -> E. y e. B x C_ y )
11 7 8 10 sylancl 
 |-  ( ( ( A e. C /\ A C_ B /\ X = Y ) /\ x e. A ) -> E. y e. B x C_ y )
12 11 ralrimiva 
 |-  ( ( A e. C /\ A C_ B /\ X = Y ) -> A. x e. A E. y e. B x C_ y )
13 1 2 isref 
 |-  ( A e. C -> ( A Ref B <-> ( Y = X /\ A. x e. A E. y e. B x C_ y ) ) )
14 13 3ad2ant1 
 |-  ( ( A e. C /\ A C_ B /\ X = Y ) -> ( A Ref B <-> ( Y = X /\ A. x e. A E. y e. B x C_ y ) ) )
15 5 12 14 mpbir2and 
 |-  ( ( A e. C /\ A C_ B /\ X = Y ) -> A Ref B )