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

Metamath Proof Explorer

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