iswun

Description: Properties of a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

		Ref	Expression
	Assertion	iswun	$⊢ U \in V \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)))$

Step	Hyp	Ref	Expression
1		treq	$⊢ u = U \to (Tr u \leftrightarrow Tr U)$
2		neeq1	$⊢ u = U \to (u \neq \emptyset \leftrightarrow U \neq \emptyset)$
3		eleq2	$⊢ u = U \to (⋃ x \in u \leftrightarrow ⋃ x \in U)$
4		eleq2	$⊢ u = U \to (𝒫 x \in u \leftrightarrow 𝒫 x \in U)$
5		eleq2	$⊢ u = U \to (\{x, y\} \in u \leftrightarrow \{x, y\} \in U)$
6	5	raleqbi1dv	$⊢ u = U \to (\forall y \in u \{x, y\} \in u \leftrightarrow \forall y \in U \{x, y\} \in U)$
7	3 4 6	3anbi123d	$⊢ u = U \to ((⋃ x \in u \land 𝒫 x \in u \land \forall y \in u \{x, y\} \in u) \leftrightarrow (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U))$
8	7	raleqbi1dv	$⊢ u = U \to (\forall x \in u (⋃ x \in u \land 𝒫 x \in u \land \forall y \in u \{x, y\} \in u) \leftrightarrow \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U))$
9	1 2 8	3anbi123d	$⊢ u = U \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)) \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)))$
10		df-wun	$⊢ WUni = \{u \| (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))\}$
11	9 10	elab2g	$⊢ U \in V \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)))$

Metamath Proof Explorer