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

Metamath Proof Explorer

Theorem axgroth5

Description: The Tarski-Grothendieck axiom using abbreviations. (Contributed by NM, 22-Jun-2009)

Ref Expression
Assertion axgroth5 ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 ax-groth ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) )
2 biid ⊢ ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 )
3 pwss ⊢ ( 𝒫 𝑧 ⊆ 𝑦 ↔ ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) )
4 pwss ⊢ ( 𝒫 𝑧 ⊆ 𝑤 ↔ ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) )
5 4 rexbii ⊢ ( ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ↔ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) )
6 3 5 anbi12i ⊢ ( ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ↔ ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) )
7 6 ralbii ⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ↔ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) )
8 df-ral ⊢ ( ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝒫 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) )
9 velpw ⊢ ( 𝑧 ∈ 𝒫 𝑦 ↔ 𝑧 ⊆ 𝑦 )
10 9 imbi1i ⊢ ( ( 𝑧 ∈ 𝒫 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) )
11 10 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝒫 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) )
12 8 11 bitri ⊢ ( ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) )
13 2 7 12 3anbi123i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) ) )
14 13 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) ) )
15 1 14 mpbir ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) )