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 ⊢∃yx∈y∧∀z∈y𝒫z⊆y∧∀f∃w∈y𝒫z⊆w∧∀i∈z∃v∈yi∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w

Proof

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