Metamath Proof Explorer

Theorem axgroth2

Description: Alternate version of the Tarski-Grothendieck Axiom. (Contributed by NM, 18-Mar-2007)

Ref Expression
Assertion axgroth2 ⊢∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y≼z∨z∈y

Proof

Step Hyp Ref Expression
1 ax-groth ⊢∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→z≈y∨z∈y
2 ssdomg ⊢y∈V→z⊆y→z≼y
3 2 elv ⊢z⊆y→z≼y
4 3 biantrurd ⊢z⊆y→y≼z↔z≼y∧y≼z
5 sbthb ⊢z≼y∧y≼z↔z≈y
6 4 5 bitrdi ⊢z⊆y→y≼z↔z≈y
7 6 orbi1d ⊢z⊆y→y≼z∨z∈y↔z≈y∨z∈y
8 7 pm5.74i ⊢z⊆y→y≼z∨z∈y↔z⊆y→z≈y∨z∈y
9 8 albii ⊢∀zz⊆y→y≼z∨z∈y↔∀zz⊆y→z≈y∨z∈y
10 9 3anbi3i ⊢x∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y≼z∨z∈y↔x∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→z≈y∨z∈y
11 10 exbii ⊢∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y≼z∨z∈y↔∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→z≈y∨z∈y
12 1 11 mpbir ⊢∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y≼z∨z∈y