# Metamath Proof Explorer

## 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 ${⊢}{A}\in \mathrm{V}$
Assertion ttukey ${⊢}\left({A}\ne \varnothing \wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔𝒫{x}\cap \mathrm{Fin}\subseteq {A}\right)\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\subset {y}$

### Proof

Step Hyp Ref Expression
1 ttukey.1 ${⊢}{A}\in \mathrm{V}$
2 1 uniex ${⊢}\bigcup {A}\in \mathrm{V}$
3 numth3 ${⊢}\bigcup {A}\in \mathrm{V}\to \bigcup {A}\in \mathrm{dom}\mathrm{card}$
4 2 3 ax-mp ${⊢}\bigcup {A}\in \mathrm{dom}\mathrm{card}$
5 ttukeyg ${⊢}\left(\bigcup {A}\in \mathrm{dom}\mathrm{card}\wedge {A}\ne \varnothing \wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔𝒫{x}\cap \mathrm{Fin}\subseteq {A}\right)\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\subset {y}$
6 4 5 mp3an1 ${⊢}\left({A}\ne \varnothing \wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔𝒫{x}\cap \mathrm{Fin}\subseteq {A}\right)\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\subset {y}$