This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tskwun

Description: A nonempty transitive Tarski class is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

		Ref	Expression
	Assertion	tskwun	$⊢ (T \in Tarski \land Tr T \land T \neq \emptyset) \to T \in WUni$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (T \in Tarski \land Tr T \land T \neq \emptyset) \to Tr T$
2		simp3	$⊢ (T \in Tarski \land Tr T \land T \neq \emptyset) \to T \neq \emptyset$
3		tskuni	$⊢ (T \in Tarski \land Tr T \land x \in T) \to ⋃ x \in T$
4	3	3expa	$⊢ ((T \in Tarski \land Tr T) \land x \in T) \to ⋃ x \in T$
5	4	3adantl3	$⊢ ((T \in Tarski \land Tr T \land T \neq \emptyset) \land x \in T) \to ⋃ x \in T$
6		tskpw	$⊢ (T \in Tarski \land x \in T) \to 𝒫 x \in T$
7	6	3ad2antl1	$⊢ ((T \in Tarski \land Tr T \land T \neq \emptyset) \land x \in T) \to 𝒫 x \in T$
8		tskpr	$⊢ (T \in Tarski \land x \in T \land y \in T) \to \{x, y\} \in T$
9	8	3exp	$⊢ T \in Tarski \to (x \in T \to (y \in T \to \{x, y\} \in T))$
10	9	3ad2ant1	$⊢ (T \in Tarski \land Tr T \land T \neq \emptyset) \to (x \in T \to (y \in T \to \{x, y\} \in T))$
11	10	imp31	$⊢ (((T \in Tarski \land Tr T \land T \neq \emptyset) \land x \in T) \land y \in T) \to \{x, y\} \in T$
12	11	ralrimiva	$⊢ ((T \in Tarski \land Tr T \land T \neq \emptyset) \land x \in T) \to \forall y \in T \{x, y\} \in T$
13	5 7 12	3jca	$⊢ ((T \in Tarski \land Tr T \land T \neq \emptyset) \land x \in T) \to (⋃ x \in T \land 𝒫 x \in T \land \forall y \in T \{x, y\} \in T)$
14	13	ralrimiva	$⊢ (T \in Tarski \land Tr T \land T \neq \emptyset) \to \forall x \in T (⋃ x \in T \land 𝒫 x \in T \land \forall y \in T \{x, y\} \in T)$
15		iswun	$⊢ T \in Tarski \to (T \in WUni \leftrightarrow (Tr T \land T \neq \emptyset \land \forall x \in T (⋃ x \in T \land 𝒫 x \in T \land \forall y \in T \{x, y\} \in T)))$
16	15	3ad2ant1	$⊢ (T \in Tarski \land Tr T \land T \neq \emptyset) \to (T \in WUni \leftrightarrow (Tr T \land T \neq \emptyset \land \forall x \in T (⋃ x \in T \land 𝒫 x \in T \land \forall y \in T \{x, y\} \in T)))$
17	1 2 14 16	mpbir3and	$⊢ (T \in Tarski \land Tr T \land T \neq \emptyset) \to T \in WUni$