Theorem ttukeyg

Description: The Teichmüller-Tukey Lemma ttukey stated with the "choice" as an antecedent (the hypothesis U. A e. dom card says that U. A is well-orderable). (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	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 )

Proof

Step	Hyp	Ref	Expression
1		n0	|- ( A =/= (/) <-> E. z z e. A )
2		ttukey2g	|- ( ( U. A e. dom card /\ z e. A /\ A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) -> E. x e. A ( z C_ x /\ A. y e. A -. x C. y ) )
3		simpr	|- ( ( z C_ x /\ A. y e. A -. x C. y ) -> A. y e. A -. x C. y )
4	3	reximi	|- ( E. x e. A ( z C_ x /\ A. y e. A -. x C. y ) -> E. x e. A A. y e. A -. x C. y )
5	2 4	syl	|- ( ( U. A e. dom card /\ z e. 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	5	3exp	|- ( U. A e. dom card -> ( z e. A -> ( A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) -> E. x e. A A. y e. A -. x C. y ) ) )
7	6	exlimdv	|- ( U. A e. dom card -> ( E. z z e. A -> ( A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) -> E. x e. A A. y e. A -. x C. y ) ) )
8	1 7	syl5bi	|- ( 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 ) ) )
9	8	3imp	|- ( ( 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 )