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 = ⋃ A$
	ssref.2	$⊢ Y = ⋃ B$
Assertion	ssref	$⊢ (A \in C \land A \subseteq B \land X = Y) \to A Ref B$

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

Metamath Proof Explorer