Theorem ttukey

Description: The Teichmüller-Tukey Lemma, an Axiom of Choice equivalent. If A is a nonempty collection of finite character, then A has a maximal element with respect to inclusion. Here "finite character" means that x e. A iff every finite subset of x is in A . (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Hypothesis	ttukey.1	⊢ 𝐴 ∈ V
Assertion	ttukey	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		ttukey.1	⊢ 𝐴 ∈ V
2	1	uniex	⊢ ∪ 𝐴 ∈ V
3		numth3	⊢ ( ∪ 𝐴 ∈ V → ∪ 𝐴 ∈ dom card )
4	2 3	ax-mp	⊢ ∪ 𝐴 ∈ dom card
5		ttukeyg	⊢ ( ( ∪ 𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )
6	4 5	mp3an1	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )