Theorem dfuniv2

Description: Alternative definition of Univ using only simple defined symbols. (Contributed by Rohan Ridenour, 10-Oct-2024)

	Ref	Expression
Assertion	dfuniv2	⊢ Univ = { 𝑦 ∣ ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) }

Proof

Step	Hyp	Ref	Expression
1		grumnueq	⊢ Univ = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
2	1	ismnu	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ Univ ↔ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑦 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) )
3	2	elv	⊢ ( 𝑦 ∈ Univ ↔ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑦 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) )
4		ismnushort	⊢ ( ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ↔ ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑦 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) )
5	4	ralbii	⊢ ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ↔ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑦 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) )
6	3 5	bitr4i	⊢ ( 𝑦 ∈ Univ ↔ ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
7	6	eqabi	⊢ Univ = { 𝑦 ∣ ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) }