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 ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 ax-groth ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) )
2 ssdomg ⊢ ( 𝑦 ∈ V → ( 𝑧 ⊆ 𝑦 → 𝑧 ≼ 𝑦 ) )
3 2 elv ⊢ ( 𝑧 ⊆ 𝑦 → 𝑧 ≼ 𝑦 )
4 3 biantrurd ⊢ ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ↔ ( 𝑧 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧 ) ) )
5 sbthb ⊢ ( ( 𝑧 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧 ) ↔ 𝑧 ≈ 𝑦 )
6 4 5 bitrdi ⊢ ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ↔ 𝑧 ≈ 𝑦 ) )
7 6 orbi1d ⊢ ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ↔ ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) )
8 7 pm5.74i ⊢ ( ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) )
9 8 albii ⊢ ( ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) )
10 9 3anbi3i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) ) )
11 10 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) ) )
12 1 11 mpbir ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )