Metamath Proof Explorer

Theorem isfne4b

Description: A condition for a topology to be finer than another. (Contributed by Jeff Hankins, 28-Sep-2009) (Revised by Mario Carneiro, 11-Sep-2015)

		Ref	Expression
	Hypotheses	isfne.1	$⊢ X = ⋃ A$
		isfne.2	$⊢ Y = ⋃ B$
	Assertion	isfne4b	$⊢ B \in V \to (A Fne B \leftrightarrow (X = Y \land topGen (A) \subseteq topGen (B)))$

Proof

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		simpr	$⊢ (B \in V \land X = Y) \to X = Y$
5	4 1 2	3eqtr3g	$⊢ (B \in V \land X = Y) \to ⋃ A = ⋃ B$
6		uniexg	$⊢ B \in V \to ⋃ B \in V$
7	6	adantr	$⊢ (B \in V \land X = Y) \to ⋃ B \in V$
8	5 7	eqeltrd	$⊢ (B \in V \land X = Y) \to ⋃ A \in V$
9		uniexb	$⊢ A \in V \leftrightarrow ⋃ A \in V$
10	8 9	sylibr	$⊢ (B \in V \land X = Y) \to A \in V$
11		simpl	$⊢ (B \in V \land X = Y) \to B \in V$
12		tgss3	$⊢ (A \in V \land B \in V) \to (topGen (A) \subseteq topGen (B) \leftrightarrow A \subseteq topGen (B))$
13	10 11 12	syl2anc	$⊢ (B \in V \land X = Y) \to (topGen (A) \subseteq topGen (B) \leftrightarrow A \subseteq topGen (B))$
14	13	pm5.32da	$⊢ B \in V \to ((X = Y \land topGen (A) \subseteq topGen (B)) \leftrightarrow (X = Y \land A \subseteq topGen (B)))$
15	3 14	bitr4id	$⊢ B \in V \to (A Fne B \leftrightarrow (X = Y \land topGen (A) \subseteq topGen (B)))$