Metamath Proof Explorer


Theorem rr-grothprimbi

Description: Express "every set is contained in a Grothendieck universe" using only primitives. The right side (without the outermost universal quantifier) is proven as rr-grothprim . (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Assertion rr-grothprimbi ( ∀ 𝑥𝑦 ∈ Univ 𝑥𝑦 ↔ ∀ 𝑥 ¬ ∀ 𝑦 ( 𝑥𝑦 → ¬ ∀ 𝑧 ( 𝑧𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑦 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑦 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 df-rex ( ∃ 𝑦 ∈ Univ 𝑥𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ Univ ∧ 𝑥𝑦 ) )
2 ancom ( ( 𝑦 ∈ Univ ∧ 𝑥𝑦 ) ↔ ( 𝑥𝑦𝑦 ∈ Univ ) )
3 biid ( 𝑥𝑦𝑥𝑦 )
4 grumnueq Univ = { 𝑘 ∣ ∀ 𝑙𝑘 ( 𝒫 𝑙𝑘 ∧ ∀ 𝑚𝑛𝑘 ( 𝒫 𝑙𝑛 ∧ ∀ 𝑝𝑙 ( ∃ 𝑞𝑘 ( 𝑝𝑞𝑞𝑚 ) → ∃ 𝑟𝑚 ( 𝑝𝑟 𝑟𝑛 ) ) ) ) }
5 4 ismnu ( 𝑦 ∈ V → ( 𝑦 ∈ Univ ↔ ∀ 𝑧𝑦 ( 𝒫 𝑧𝑦 ∧ ∀ 𝑓𝑤𝑦 ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑦 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) ) )
6 5 elv ( 𝑦 ∈ Univ ↔ ∀ 𝑧𝑦 ( 𝒫 𝑧𝑦 ∧ ∀ 𝑓𝑤𝑦 ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑦 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) )
7 ismnuprim ( ∀ 𝑧𝑦 ( 𝒫 𝑧𝑦 ∧ ∀ 𝑓𝑤𝑦 ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑦 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) ↔ ∀ 𝑧 ( 𝑧𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑦 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑦 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) ) ) )
8 6 7 bitri ( 𝑦 ∈ Univ ↔ ∀ 𝑧 ( 𝑧𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑦 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑦 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) ) ) )
9 3 8 expandan ( ( 𝑥𝑦𝑦 ∈ Univ ) ↔ ¬ ( 𝑥𝑦 → ¬ ∀ 𝑧 ( 𝑧𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑦 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑦 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) ) ) ) )
10 2 9 bitri ( ( 𝑦 ∈ Univ ∧ 𝑥𝑦 ) ↔ ¬ ( 𝑥𝑦 → ¬ ∀ 𝑧 ( 𝑧𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑦 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑦 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) ) ) ) )
11 10 expandexn ( ∃ 𝑦 ( 𝑦 ∈ Univ ∧ 𝑥𝑦 ) ↔ ¬ ∀ 𝑦 ( 𝑥𝑦 → ¬ ∀ 𝑧 ( 𝑧𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑦 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑦 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) ) ) ) )
12 1 11 bitri ( ∃ 𝑦 ∈ Univ 𝑥𝑦 ↔ ¬ ∀ 𝑦 ( 𝑥𝑦 → ¬ ∀ 𝑧 ( 𝑧𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑦 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑦 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) ) ) ) )
13 12 albii ( ∀ 𝑥𝑦 ∈ Univ 𝑥𝑦 ↔ ∀ 𝑥 ¬ ∀ 𝑦 ( 𝑥𝑦 → ¬ ∀ 𝑧 ( 𝑧𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑦 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑦 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) ) ) ) )