mnutrd

Description: Minimal universes are transitive. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypotheses	mnutrd.1	$⊢ M = \{k \| \forall l \in k (𝒫 l \subseteq k \land \forall m \exists n \in k (𝒫 l \subseteq n \land \forall p \in l (\exists q \in k (p \in q \land q \in m) \to \exists r \in m (p \in r \land ⋃ r \subseteq n))))\}$
	mnutrd.2	$⊢ φ \to U \in M$
Assertion	mnutrd	$⊢ φ \to Tr U$

Step	Hyp	Ref	Expression
1		mnutrd.1	$⊢ M = \{k \| \forall l \in k (𝒫 l \subseteq k \land \forall m \exists n \in k (𝒫 l \subseteq n \land \forall p \in l (\exists q \in k (p \in q \land q \in m) \to \exists r \in m (p \in r \land ⋃ r \subseteq n))))\}$
2		mnutrd.2	$⊢ φ \to U \in M$
3	2	adantr	$⊢ (φ \land (x \in y \land y \in U)) \to U \in M$
4		simprr	$⊢ (φ \land (x \in y \land y \in U)) \to y \in U$
5		simprl	$⊢ (φ \land (x \in y \land y \in U)) \to x \in y$
6	1 3 4 5	mnutrcld	$⊢ (φ \land (x \in y \land y \in U)) \to x \in U$
7	6	ex	$⊢ φ \to ((x \in y \land y \in U) \to x \in U)$
8	7	alrimivv	$⊢ φ \to \forall x \forall y ((x \in y \land y \in U) \to x \in U)$
9		dftr2	$⊢ Tr U \leftrightarrow \forall x \forall y ((x \in y \land y \in U) \to x \in U)$
10	8 9	sylibr	$⊢ φ \to Tr U$

Metamath Proof Explorer