isfne4

Description: The predicate " B is finer than A " in terms of the topology generation function. (Contributed by Mario Carneiro, 11-Sep-2015)

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

Step	Hyp	Ref	Expression
1		isfne.1	$⊢ X = ⋃ A$
2		isfne.2	$⊢ Y = ⋃ B$
3		fnerel	$⊢ Rel Fne$
4	3	brrelex2i	$⊢ A Fne B \to B \in V$
5		simpl	$⊢ (X = Y \land A \subseteq topGen (B)) \to X = Y$
6	5 1 2	3eqtr3g	$⊢ (X = Y \land A \subseteq topGen (B)) \to ⋃ A = ⋃ B$
7		fvex	$⊢ topGen (B) \in V$
8	7	ssex	$⊢ A \subseteq topGen (B) \to A \in V$
9	8	adantl	$⊢ (X = Y \land A \subseteq topGen (B)) \to A \in V$
10	9	uniexd	$⊢ (X = Y \land A \subseteq topGen (B)) \to ⋃ A \in V$
11	6 10	eqeltrrd	$⊢ (X = Y \land A \subseteq topGen (B)) \to ⋃ B \in V$
12		uniexb	$⊢ B \in V \leftrightarrow ⋃ B \in V$
13	11 12	sylibr	$⊢ (X = Y \land A \subseteq topGen (B)) \to B \in V$
14	1 2	isfne	$⊢ B \in V \to (A Fne B \leftrightarrow (X = Y \land \forall x \in A x \subseteq ⋃ (B \cap 𝒫 x)))$
15		dfss3	$⊢ A \subseteq topGen (B) \leftrightarrow \forall x \in A x \in topGen (B)$
16		eltg	$⊢ B \in V \to (x \in topGen (B) \leftrightarrow x \subseteq ⋃ (B \cap 𝒫 x))$
17	16	ralbidv	$⊢ B \in V \to (\forall x \in A x \in topGen (B) \leftrightarrow \forall x \in A x \subseteq ⋃ (B \cap 𝒫 x))$
18	15 17	bitrid	$⊢ B \in V \to (A \subseteq topGen (B) \leftrightarrow \forall x \in A x \subseteq ⋃ (B \cap 𝒫 x))$
19	18	anbi2d	$⊢ B \in V \to ((X = Y \land A \subseteq topGen (B)) \leftrightarrow (X = Y \land \forall x \in A x \subseteq ⋃ (B \cap 𝒫 x)))$
20	14 19	bitr4d	$⊢ B \in V \to (A Fne B \leftrightarrow (X = Y \land A \subseteq topGen (B)))$
21	4 13 20	pm5.21nii	$⊢ A Fne B \leftrightarrow (X = Y \land A \subseteq topGen (B))$

Metamath Proof Explorer