Theorem mnutrd

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

	Ref	Expression
Hypotheses	mnutrd.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
	mnutrd.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
Assertion	mnutrd	⊢ ( 𝜑 → Tr 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		mnutrd.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
2		mnutrd.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
3	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑈 ∈ 𝑀 )
4		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑈 )
5		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ 𝑦 )
6	1 3 4 5	mnutrcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ 𝑈 )
7	6	ex	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 ) )
8	7	alrimivv	⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 ) )
9		dftr2	⊢ ( Tr 𝑈 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 ) )
10	8 9	sylibr	⊢ ( 𝜑 → Tr 𝑈 )