wununi

Description: A weak universe is closed under union. (Contributed by Mario Carneiro, 2-Jan-2017)

Step	Hyp	Ref	Expression
1		wununi.1	$⊢ φ \to U \in WUni$
2		wununi.2	$⊢ φ \to A \in U$
3		unieq	$⊢ x = A \to ⋃ x = ⋃ A$
4	3	eleq1d	$⊢ x = A \to (⋃ x \in U \leftrightarrow ⋃ A \in U)$
5		iswun	$⊢ U \in WUni \to (U \in WUni \leftrightarrow (Tr U \land U \neq \emptyset \land \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U)))$
6	5	ibi	$⊢ U \in WUni \to (Tr U \land U \neq \emptyset \land \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U))$
7	6	simp3d	$⊢ U \in WUni \to \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U)$
8		simp1	$⊢ (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U) \to ⋃ x \in U$
9	8	ralimi	$⊢ \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U) \to \forall x \in U ⋃ x \in U$
10	1 7 9	3syl	$⊢ φ \to \forall x \in U ⋃ x \in U$
11	4 10 2	rspcdva	$⊢ φ \to ⋃ A \in U$

Metamath Proof Explorer