Metamath Proof Explorer

Theorem fness

Description: A cover is finer than its subcovers. (Contributed by Jeff Hankins, 11-Oct-2009)

		Ref	Expression
	Hypotheses	fness.1	$⊢ X = ⋃ A$
		fness.2	$⊢ Y = ⋃ B$
	Assertion	fness	$⊢ (B \in C \land A \subseteq B \land X = Y) \to A Fne B$

Proof

Step	Hyp	Ref	Expression
1		fness.1	$⊢ X = ⋃ A$
2		fness.2	$⊢ Y = ⋃ B$
3		simp3	$⊢ (B \in C \land A \subseteq B \land X = Y) \to X = Y$
4		ssel2	$⊢ (A \subseteq B \land x \in A) \to x \in B$
5	4	3adant3	$⊢ (A \subseteq B \land x \in A \land y \in x) \to x \in B$
6		simp3	$⊢ (A \subseteq B \land x \in A \land y \in x) \to y \in x$
7		ssid	$⊢ x \subseteq x$
8	6 7	jctir	$⊢ (A \subseteq B \land x \in A \land y \in x) \to (y \in x \land x \subseteq x)$
9		elequ2	$⊢ z = x \to (y \in z \leftrightarrow y \in x)$
10		sseq1	$⊢ z = x \to (z \subseteq x \leftrightarrow x \subseteq x)$
11	9 10	anbi12d	$⊢ z = x \to ((y \in z \land z \subseteq x) \leftrightarrow (y \in x \land x \subseteq x))$
12	11	rspcev	$⊢ (x \in B \land (y \in x \land x \subseteq x)) \to \exists z \in B (y \in z \land z \subseteq x)$
13	5 8 12	syl2anc	$⊢ (A \subseteq B \land x \in A \land y \in x) \to \exists z \in B (y \in z \land z \subseteq x)$
14	13	3expib	$⊢ A \subseteq B \to ((x \in A \land y \in x) \to \exists z \in B (y \in z \land z \subseteq x))$
15	14	ralrimivv	$⊢ A \subseteq B \to \forall x \in A \forall y \in x \exists z \in B (y \in z \land z \subseteq x)$
16	15	3ad2ant2	$⊢ (B \in C \land A \subseteq B \land X = Y) \to \forall x \in A \forall y \in x \exists z \in B (y \in z \land z \subseteq x)$
17	1 2	isfne2	$⊢ B \in C \to (A Fne B \leftrightarrow (X = Y \land \forall x \in A \forall y \in x \exists z \in B (y \in z \land z \subseteq x)))$
18	17	3ad2ant1	$⊢ (B \in C \land A \subseteq B \land X = Y) \to (A Fne B \leftrightarrow (X = Y \land \forall x \in A \forall y \in x \exists z \in B (y \in z \land z \subseteq x)))$
19	3 16 18	mpbir2and	$⊢ (B \in C \land A \subseteq B \land X = Y) \to A Fne B$