Theorem grumnud

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

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

Proof

Step	Hyp	Ref	Expression
1		grumnud.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
2		grumnud.2	⊢ ( 𝜑 → 𝐺 ∈ Univ )
3		eqid	⊢ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) = ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) )
4		brxp	⊢ ( 𝑖 ( 𝐺 × 𝐺 ) ℎ ↔ ( 𝑖 ∈ 𝐺 ∧ ℎ ∈ 𝐺 ) )
5		brin	⊢ ( 𝑖 ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) ℎ ↔ ( 𝑖 { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ℎ ∧ 𝑖 ( 𝐺 × 𝐺 ) ℎ ) )
6	5	rbaib	⊢ ( 𝑖 ( 𝐺 × 𝐺 ) ℎ → ( 𝑖 ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) ℎ ↔ 𝑖 { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ℎ ) )
7	4 6	sylbir	⊢ ( ( 𝑖 ∈ 𝐺 ∧ ℎ ∈ 𝐺 ) → ( 𝑖 ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) ℎ ↔ 𝑖 { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ℎ ) )
8		vex	⊢ 𝑖 ∈ V
9		vex	⊢ ℎ ∈ V
10		simpr	⊢ ( ( ( 𝑏 = 𝑖 ∧ 𝑐 = ℎ ) ∧ 𝑑 = 𝑗 ) → 𝑑 = 𝑗 )
11	10	unieqd	⊢ ( ( ( 𝑏 = 𝑖 ∧ 𝑐 = ℎ ) ∧ 𝑑 = 𝑗 ) → ∪ 𝑑 = ∪ 𝑗 )
12		simplr	⊢ ( ( ( 𝑏 = 𝑖 ∧ 𝑐 = ℎ ) ∧ 𝑑 = 𝑗 ) → 𝑐 = ℎ )
13	11 12	eqeq12d	⊢ ( ( ( 𝑏 = 𝑖 ∧ 𝑐 = ℎ ) ∧ 𝑑 = 𝑗 ) → ( ∪ 𝑑 = 𝑐 ↔ ∪ 𝑗 = ℎ ) )
14		elequ1	⊢ ( 𝑑 = 𝑗 → ( 𝑑 ∈ 𝑓 ↔ 𝑗 ∈ 𝑓 ) )
15	14	adantl	⊢ ( ( ( 𝑏 = 𝑖 ∧ 𝑐 = ℎ ) ∧ 𝑑 = 𝑗 ) → ( 𝑑 ∈ 𝑓 ↔ 𝑗 ∈ 𝑓 ) )
16		eleq12	⊢ ( ( 𝑏 = 𝑖 ∧ 𝑑 = 𝑗 ) → ( 𝑏 ∈ 𝑑 ↔ 𝑖 ∈ 𝑗 ) )
17	16	adantlr	⊢ ( ( ( 𝑏 = 𝑖 ∧ 𝑐 = ℎ ) ∧ 𝑑 = 𝑗 ) → ( 𝑏 ∈ 𝑑 ↔ 𝑖 ∈ 𝑗 ) )
18	13 15 17	3anbi123d	⊢ ( ( ( 𝑏 = 𝑖 ∧ 𝑐 = ℎ ) ∧ 𝑑 = 𝑗 ) → ( ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) ↔ ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) )
19	18	cbvexdvaw	⊢ ( ( 𝑏 = 𝑖 ∧ 𝑐 = ℎ ) → ( ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) ↔ ∃ 𝑗 ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) )
20		eqid	⊢ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } = { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) }
21	8 9 19 20	braba	⊢ ( 𝑖 { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ℎ ↔ ∃ 𝑗 ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) )
22	7 21	bitrdi	⊢ ( ( 𝑖 ∈ 𝐺 ∧ ℎ ∈ 𝐺 ) → ( 𝑖 ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) ℎ ↔ ∃ 𝑗 ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) )
23		simplr3	⊢ ( ( ( ℎ ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) ∧ ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) ∧ 𝑢 = 𝑗 ) → 𝑖 ∈ 𝑗 )
24		simpr	⊢ ( ( ( ℎ ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) ∧ ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) ∧ 𝑢 = 𝑗 ) → 𝑢 = 𝑗 )
25	23 24	eleqtrrd	⊢ ( ( ( ℎ ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) ∧ ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) ∧ 𝑢 = 𝑗 ) → 𝑖 ∈ 𝑢 )
26	24	unieqd	⊢ ( ( ( ℎ ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) ∧ ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) ∧ 𝑢 = 𝑗 ) → ∪ 𝑢 = ∪ 𝑗 )
27		simplr1	⊢ ( ( ( ℎ ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) ∧ ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) ∧ 𝑢 = 𝑗 ) → ∪ 𝑗 = ℎ )
28	26 27	eqtrd	⊢ ( ( ( ℎ ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) ∧ ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) ∧ 𝑢 = 𝑗 ) → ∪ 𝑢 = ℎ )
29		simpll	⊢ ( ( ( ℎ ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) ∧ ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) ∧ 𝑢 = 𝑗 ) → ℎ ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) )
30	28 29	eqeltrd	⊢ ( ( ( ℎ ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) ∧ ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) ∧ 𝑢 = 𝑗 ) → ∪ 𝑢 ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) )
31	25 30	jca	⊢ ( ( ( ℎ ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) ∧ ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) ∧ 𝑢 = 𝑗 ) → ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) ) )
32		simpr2	⊢ ( ( ℎ ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) ∧ ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) → 𝑗 ∈ 𝑓 )
33	31 32	rspcime	⊢ ( ( ℎ ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) ∧ ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) Coll 𝑧 ) ) )
34	1 2 3 22 33	grumnudlem	⊢ ( 𝜑 → 𝐺 ∈ 𝑀 )