Theorem rr-grothprim

Description: An equivalent of ax-groth using only primitives. This uses only 123 symbols, which is significantly less than the previous record of 163 established by grothprim (which uses some defined symbols, and requires 229 symbols if expanded to primitives). (Contributed by Rohan Ridenour, 13-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		gruex	⊢ ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦
2	1	ax-gen	⊢ ∀ 𝑥 ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦
3		rr-grothprimbi	⊢ ( ∀ 𝑥 ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∀ 𝑥 ¬ ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧 ) → ¬ ( 𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖 ∈ 𝑧 → ( 𝑣 ∈ 𝑦 → ( 𝑖 ∈ 𝑣 → ( 𝑣 ∈ 𝑓 → ¬ ∀ 𝑢 ( 𝑢 ∈ 𝑓 → ( 𝑖 ∈ 𝑢 → ¬ ∀ 𝑜 ( 𝑜 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤 ) ) ) ) ) ) ) ) ) ) ) ) )
4	2 3	mpbi	⊢ ∀ 𝑥 ¬ ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧 ) → ¬ ( 𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖 ∈ 𝑧 → ( 𝑣 ∈ 𝑦 → ( 𝑖 ∈ 𝑣 → ( 𝑣 ∈ 𝑓 → ¬ ∀ 𝑢 ( 𝑢 ∈ 𝑓 → ( 𝑖 ∈ 𝑢 → ¬ ∀ 𝑜 ( 𝑜 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤 ) ) ) ) ) ) ) ) ) ) ) )
5	4	spi	⊢ ¬ ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧 ) → ¬ ( 𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖 ∈ 𝑧 → ( 𝑣 ∈ 𝑦 → ( 𝑖 ∈ 𝑣 → ( 𝑣 ∈ 𝑓 → ¬ ∀ 𝑢 ( 𝑢 ∈ 𝑓 → ( 𝑖 ∈ 𝑢 → ¬ ∀ 𝑜 ( 𝑜 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤 ) ) ) ) ) ) ) ) ) ) ) )