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 )