fneuni

Description: If B is finer than A , every element of A is a union of elements of B . (Contributed by Jeff Hankins, 11-Oct-2009)

		Ref	Expression
	Assertion	fneuni	$⊢ (A Fne B \land S \in A) \to \exists x (x \subseteq B \land S = ⋃ x)$

Step	Hyp	Ref	Expression
1		fnetg	$⊢ A Fne B \to A \subseteq topGen (B)$
2	1	sselda	$⊢ (A Fne B \land S \in A) \to S \in topGen (B)$
3		elfvdm	$⊢ S \in topGen (B) \to B \in dom topGen$
4		eltg3	$⊢ B \in dom topGen \to (S \in topGen (B) \leftrightarrow \exists x (x \subseteq B \land S = ⋃ x))$
5	3 4	syl	$⊢ S \in topGen (B) \to (S \in topGen (B) \leftrightarrow \exists x (x \subseteq B \land S = ⋃ x))$
6	5	ibi	$⊢ S \in topGen (B) \to \exists x (x \subseteq B \land S = ⋃ x)$
7	2 6	syl	$⊢ (A Fne B \land S \in A) \to \exists x (x \subseteq B \land S = ⋃ x)$

Metamath Proof Explorer