unidif

Description: If the difference A \ B contains the largest members of A , then the union of the difference is the union of A . (Contributed by NM, 22-Mar-2004)

		Ref	Expression
	Assertion	unidif	$⊢ \forall x \in A \exists y \in (A ∖ B) x \subseteq y \to ⋃ (A ∖ B) = ⋃ A$

Proof

Step	Hyp	Ref	Expression
1		uniss2	$⊢ \forall x \in A \exists y \in (A ∖ B) x \subseteq y \to ⋃ A \subseteq ⋃ (A ∖ B)$
2		difss	$⊢ A ∖ B \subseteq A$
3	2	unissi	$⊢ ⋃ (A ∖ B) \subseteq ⋃ A$
4	1 3	jctil	$⊢ \forall x \in A \exists y \in (A ∖ B) x \subseteq y \to (⋃ (A ∖ B) \subseteq ⋃ A \land ⋃ A \subseteq ⋃ (A ∖ B))$
5		eqss	$⊢ ⋃ (A ∖ B) = ⋃ A \leftrightarrow (⋃ (A ∖ B) \subseteq ⋃ A \land ⋃ A \subseteq ⋃ (A ∖ B))$
6	4 5	sylibr	$⊢ \forall x \in A \exists y \in (A ∖ B) x \subseteq y \to ⋃ (A ∖ B) = ⋃ A$

Metamath Proof Explorer

Theorem unidif

Proof