Theorem rr-grothshortbi

Description: Express "every set is contained in a Grothendieck universe" in a short form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 8-Oct-2024)

	Ref	Expression
Assertion	rr-grothshortbi	⊢ ( ∀ 𝑥 ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∀ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-rex	⊢ ( ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ Univ ∧ 𝑥 ∈ 𝑦 ) )
2		exancom	⊢ ( ∃ 𝑦 ( 𝑦 ∈ Univ ∧ 𝑥 ∈ 𝑦 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ Univ ) )
3		dfuniv2	⊢ Univ = { 𝑦 ∣ ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) }
4	3	eqabri	⊢ ( 𝑦 ∈ Univ ↔ ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
5	4	anbi2i	⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ Univ ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ) )
6	5	exbii	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ Univ ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ) )
7	1 2 6	3bitri	⊢ ( ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ) )
8	7	albii	⊢ ( ∀ 𝑥 ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∀ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ) )