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=\bigcup A$$
	ssref.2	$$⊢Y=\bigcup B$$
Assertion	ssref	$$⊢\left(A\in C\wedge A\subseteq B\wedge X=Y\right)\to A\mathrm{Ref}B$$

Proof

Step	Hyp	Ref	Expression
1		ssref.1	$$⊢X=\bigcup A$$
2		ssref.2	$$⊢Y=\bigcup B$$
3		eqcom	$$⊢X=Y\leftrightarrow Y=X$$
4	3	biimpi	$$⊢X=Y\to Y=X$$
5	4	3ad2ant3	$$⊢\left(A\in C\wedge A\subseteq B\wedge X=Y\right)\to Y=X$$
6		ssel2	$$⊢\left(A\subseteq B\wedge x\in A\right)\to x\in B$$
7	6	3ad2antl2	$$⊢\left(\left(A\in C\wedge A\subseteq B\wedge X=Y\right)\wedge x\in A\right)\to x\in B$$
8		ssid	$$⊢x\subseteq x$$
9		sseq2	$$⊢y=x\to \left(x\subseteq y\leftrightarrow x\subseteq x\right)$$
10	9	rspcev	$$⊢\left(x\in B\wedge x\subseteq x\right)\to \exists y\in Bx\subseteq y$$
11	7 8 10	sylancl	$$⊢\left(\left(A\in C\wedge A\subseteq B\wedge X=Y\right)\wedge x\in A\right)\to \exists y\in Bx\subseteq y$$
12	11	ralrimiva	$$⊢\left(A\in C\wedge A\subseteq B\wedge X=Y\right)\to \forall x\in A\exists y\in Bx\subseteq y$$
13	1 2	isref	$$⊢A\in C\to \left(A\mathrm{Ref}B\leftrightarrow \left(Y=X\wedge \forall x\in A\exists y\in Bx\subseteq y\right)\right)$$
14	13	3ad2ant1	$$⊢\left(A\in C\wedge A\subseteq B\wedge X=Y\right)\to \left(A\mathrm{Ref}B\leftrightarrow \left(Y=X\wedge \forall x\in A\exists y\in Bx\subseteq y\right)\right)$$
15	5 12 14	mpbir2and	$$⊢\left(A\in C\wedge A\subseteq B\wedge X=Y\right)\to A\mathrm{Ref}B$$