Metamath Proof Explorer

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 ⊢ ¬ ∀ y x ∈ y → ¬ ∀ z z ∈ y → ∀ f ¬ ∀ w w ∈ y → ¬ ∀ v ¬ ∀ t t ∈ v → t ∈ z → ¬ v ∈ y → ¬ v ∈ w → ¬ ∀ i i ∈ z → v ∈ y → i ∈ v → v ∈ f → ¬ ∀ u u ∈ f → i ∈ u → ¬ ∀ o o ∈ u → ∀ s s ∈ o → s ∈ w

Proof

Step Hyp Ref Expression
1 gruex ⊢ ∃ y ∈ Univ x ∈ y
2 1 ax-gen ⊢ ∀ x ∃ y ∈ Univ x ∈ y
3 rr-grothprimbi ⊢ ∀ x ∃ y ∈ Univ x ∈ y ↔ ∀ x ¬ ∀ y x ∈ y → ¬ ∀ z z ∈ y → ∀ f ¬ ∀ w w ∈ y → ¬ ∀ v ¬ ∀ t t ∈ v → t ∈ z → ¬ v ∈ y → ¬ v ∈ w → ¬ ∀ i i ∈ z → v ∈ y → i ∈ v → v ∈ f → ¬ ∀ u u ∈ f → i ∈ u → ¬ ∀ o o ∈ u → ∀ s s ∈ o → s ∈ w
4 2 3 mpbi ⊢ ∀ x ¬ ∀ y x ∈ y → ¬ ∀ z z ∈ y → ∀ f ¬ ∀ w w ∈ y → ¬ ∀ v ¬ ∀ t t ∈ v → t ∈ z → ¬ v ∈ y → ¬ v ∈ w → ¬ ∀ i i ∈ z → v ∈ y → i ∈ v → v ∈ f → ¬ ∀ u u ∈ f → i ∈ u → ¬ ∀ o o ∈ u → ∀ s s ∈ o → s ∈ w
5 4 spi ⊢ ¬ ∀ y x ∈ y → ¬ ∀ z z ∈ y → ∀ f ¬ ∀ w w ∈ y → ¬ ∀ v ¬ ∀ t t ∈ v → t ∈ z → ¬ v ∈ y → ¬ v ∈ w → ¬ ∀ i i ∈ z → v ∈ y → i ∈ v → v ∈ f → ¬ ∀ u u ∈ f → i ∈ u → ¬ ∀ o o ∈ u → ∀ s s ∈ o → s ∈ w