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 e. _V
Assertion	ttukey	|- ( ( A =/= (/) /\ A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) -> E. x e. A A. y e. A -. x C. y )

Proof

Step	Hyp	Ref	Expression
1		ttukey.1	|- A e. _V
2	1	uniex	|- U. A e. _V
3		numth3	|- ( U. A e. _V -> U. A e. dom card )
4	2 3	ax-mp	|- U. A e. dom card
5		ttukeyg	|- ( ( U. A e. dom card /\ A =/= (/) /\ A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) -> E. x e. A A. y e. A -. x C. y )
6	4 5	mp3an1	|- ( ( A =/= (/) /\ A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) -> E. x e. A A. y e. A -. x C. y )