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\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\right)\to \exists x\in A\forall y\in A\neg 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\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\right)\to \exists x\in A\forall y\in A\neg x\subset y$$
6	4 5	mp3an1	$$⊢\left(A\ne \varnothing \wedge \forall x\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\right)\to \exists x\in A\forall y\in A\neg x\subset y$$