Theorem mnugrud

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

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

Proof

Step	Hyp	Ref	Expression
1		mnugrud.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
2		mnugrud.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
3	1 2	mnutrd	⊢ ( 𝜑 → Tr 𝑈 )
4	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑈 ∈ 𝑀 )
5		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 )
6	1 4 5	mnupwd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝒫 𝑥 ∈ 𝑈 )
7	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝑈 ) → 𝑈 ∈ 𝑀 )
8	5	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 )
9		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝑈 ) → 𝑦 ∈ 𝑈 )
10	1 7 8 9	mnuprd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝑈 ) → { 𝑥 , 𝑦 } ∈ 𝑈 )
11	10	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 )
12	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ) → 𝑈 ∈ 𝑀 )
13	5	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ) → 𝑥 ∈ 𝑈 )
14		elmapi	⊢ ( 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) → 𝑦 : 𝑥 ⟶ 𝑈 )
15	14	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ) → 𝑦 : 𝑥 ⟶ 𝑈 )
16	1 12 13 15	mnurnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ) → ran 𝑦 ∈ 𝑈 )
17	1 12 16	mnuunid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ) → ∪ ran 𝑦 ∈ 𝑈 )
18	17	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 )
19	6 11 18	3jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) )
20	19	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) )
21		elgrug	⊢ ( 𝑈 ∈ 𝑀 → ( 𝑈 ∈ Univ ↔ ( Tr 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) ) ) )
22	2 21	syl	⊢ ( 𝜑 → ( 𝑈 ∈ Univ ↔ ( Tr 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) ) ) )
23	3 20 22	mpbir2and	⊢ ( 𝜑 → 𝑈 ∈ Univ )