This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axgroth2

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

Ref Expression
Assertion axgroth2 ⊢ ∃ y x ∈ y ∧ ∀ z ∈ y ∀ w w ⊆ z → w ∈ y ∧ ∃ w ∈ y ∀ v v ⊆ z → v ∈ w ∧ ∀ z z ⊆ y → y ≼ z ∨ z ∈ y

Proof

Step Hyp Ref Expression
1 ax-groth ⊢ ∃ y x ∈ y ∧ ∀ z ∈ y ∀ w w ⊆ z → w ∈ y ∧ ∃ w ∈ y ∀ v v ⊆ z → v ∈ w ∧ ∀ z z ⊆ 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 ⊢ ∀ z z ⊆ y → y ≼ z ∨ z ∈ y ↔ ∀ z z ⊆ y → z ≈ y ∨ z ∈ y
10 9 3anbi3i ⊢ x ∈ y ∧ ∀ z ∈ y ∀ w w ⊆ z → w ∈ y ∧ ∃ w ∈ y ∀ v v ⊆ z → v ∈ w ∧ ∀ z z ⊆ y → y ≼ z ∨ z ∈ y ↔ x ∈ y ∧ ∀ z ∈ y ∀ w w ⊆ z → w ∈ y ∧ ∃ w ∈ y ∀ v v ⊆ z → v ∈ w ∧ ∀ z z ⊆ y → z ≈ y ∨ z ∈ y
11 10 exbii ⊢ ∃ y x ∈ y ∧ ∀ z ∈ y ∀ w w ⊆ z → w ∈ y ∧ ∃ w ∈ y ∀ v v ⊆ z → v ∈ w ∧ ∀ z z ⊆ y → y ≼ z ∨ z ∈ y ↔ ∃ y x ∈ y ∧ ∀ z ∈ y ∀ w w ⊆ z → w ∈ y ∧ ∃ w ∈ y ∀ v v ⊆ z → v ∈ w ∧ ∀ z z ⊆ y → z ≈ y ∨ z ∈ y
12 1 11 mpbir ⊢ ∃ y x ∈ y ∧ ∀ z ∈ y ∀ w w ⊆ z → w ∈ y ∧ ∃ w ∈ y ∀ v v ⊆ z → v ∈ w ∧ ∀ z z ⊆ y → y ≼ z ∨ z ∈ y