isfne2

Description: The predicate " B is finer than A ". (Contributed by Jeff Hankins, 28-Sep-2009) (Proof shortened by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	isfne.1	$⊢ X = ⋃ A$
	isfne.2	$⊢ Y = ⋃ B$
Assertion	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)))$

Step	Hyp	Ref	Expression
1		isfne.1	$⊢ X = ⋃ A$
2		isfne.2	$⊢ Y = ⋃ B$
3	1 2	isfne4	$⊢ A Fne B \leftrightarrow (X = Y \land A \subseteq topGen (B))$
4		dfss3	$⊢ A \subseteq topGen (B) \leftrightarrow \forall x \in A x \in topGen (B)$
5		eltg2b	$⊢ B \in C \to (x \in topGen (B) \leftrightarrow \forall y \in x \exists z \in B (y \in z \land z \subseteq x))$
6	5	ralbidv	$⊢ B \in C \to (\forall x \in A x \in topGen (B) \leftrightarrow \forall x \in A \forall y \in x \exists z \in B (y \in z \land z \subseteq x))$
7	4 6	bitrid	$⊢ B \in C \to (A \subseteq topGen (B) \leftrightarrow \forall x \in A \forall y \in x \exists z \in B (y \in z \land z \subseteq x))$
8	7	anbi2d	$⊢ B \in C \to ((X = Y \land A \subseteq topGen (B)) \leftrightarrow (X = Y \land \forall x \in A \forall y \in x \exists z \in B (y \in z \land z \subseteq x)))$
9	3 8	bitrid	$⊢ 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)))$

Metamath Proof Explorer