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