Metamath Proof Explorer

Theorem rr-groth

Description: An equivalent of ax-groth using only simple defined symbols. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Assertion rr-groth ⊢ ∃ y x ∈ y ∧ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∀ f ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ y i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w

Proof

Step Hyp Ref Expression
1 gruex ⊢ ∃ y ∈ Univ x ∈ y
2 df-rex ⊢ ∃ y ∈ Univ x ∈ y ↔ ∃ y y ∈ Univ ∧ x ∈ y
3 exancom ⊢ ∃ y y ∈ Univ ∧ x ∈ y ↔ ∃ y x ∈ y ∧ y ∈ Univ
4 grumnueq ⊢ Univ = k | ∀ l ∈ k 𝒫 l ⊆ k ∧ ∀ m ∃ n ∈ k 𝒫 l ⊆ n ∧ ∀ p ∈ l ∃ q ∈ k p ∈ q ∧ q ∈ m → ∃ r ∈ m p ∈ r ∧ ⋃ r ⊆ n
5 4 ismnu ⊢ y ∈ V → y ∈ Univ ↔ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∀ f ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ y i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
6 5 elv ⊢ y ∈ Univ ↔ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∀ f ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ y i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
7 6 anbi2i ⊢ x ∈ y ∧ y ∈ Univ ↔ x ∈ y ∧ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∀ f ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ y i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
8 7 exbii ⊢ ∃ y x ∈ y ∧ y ∈ Univ ↔ ∃ y x ∈ y ∧ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∀ f ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ y i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
9 2 3 8 3bitri ⊢ ∃ y ∈ Univ x ∈ y ↔ ∃ y x ∈ y ∧ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∀ f ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ y i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
10 1 9 mpbi ⊢ ∃ y x ∈ y ∧ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∀ f ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ y i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w