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

Metamath Proof Explorer

Theorem weth

Description: Well-ordering theorem: any set A can be well-ordered. This is an equivalent of the Axiom of Choice. Theorem 6 of Suppes p. 242. First proved by Ernst Zermelo (the "Z" in ZFC) in 1904. (Contributed by Mario Carneiro, 5-Jan-2013)

		Ref	Expression
	Assertion	weth	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 We 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		weeq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 We 𝑦 ↔ 𝑥 We 𝐴 ) )
2	1	exbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 𝑥 We 𝑦 ↔ ∃ 𝑥 𝑥 We 𝐴 ) )
3		dfac8	⊢ ( CHOICE ↔ ∀ 𝑦 ∃ 𝑥 𝑥 We 𝑦 )
4	3	axaci	⊢ ∃ 𝑥 𝑥 We 𝑦
5	2 4	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 We 𝐴 )