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

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 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 )