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	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) )