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

Metamath Proof Explorer

Theorem ttukeylem2

Description: Lemma for ttukey . A property of finite character is closed under subsets. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Hypotheses ttukeylem.1 
|- ( ph -> F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) )
ttukeylem.2 
|- ( ph -> B e. A )
ttukeylem.3 
|- ( ph -> A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) )
Assertion ttukeylem2 
|- ( ( ph /\ ( C e. A /\ D C_ C ) ) -> D e. A )

Proof

Step Hyp Ref Expression
1 ttukeylem.1 
 |-  ( ph -> F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) )
2 ttukeylem.2 
 |-  ( ph -> B e. A )
3 ttukeylem.3 
 |-  ( ph -> A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) )
4 simpr 
 |-  ( ( ph /\ D C_ C ) -> D C_ C )
5 4 sspwd 
 |-  ( ( ph /\ D C_ C ) -> ~P D C_ ~P C )
6 ssrin 
 |-  ( ~P D C_ ~P C -> ( ~P D i^i Fin ) C_ ( ~P C i^i Fin ) )
7 sstr2 
 |-  ( ( ~P D i^i Fin ) C_ ( ~P C i^i Fin ) -> ( ( ~P C i^i Fin ) C_ A -> ( ~P D i^i Fin ) C_ A ) )
8 5 6 7 3syl 
 |-  ( ( ph /\ D C_ C ) -> ( ( ~P C i^i Fin ) C_ A -> ( ~P D i^i Fin ) C_ A ) )
9 1 2 3 ttukeylem1 
 |-  ( ph -> ( C e. A <-> ( ~P C i^i Fin ) C_ A ) )
10 9 adantr 
 |-  ( ( ph /\ D C_ C ) -> ( C e. A <-> ( ~P C i^i Fin ) C_ A ) )
11 1 2 3 ttukeylem1 
 |-  ( ph -> ( D e. A <-> ( ~P D i^i Fin ) C_ A ) )
12 11 adantr 
 |-  ( ( ph /\ D C_ C ) -> ( D e. A <-> ( ~P D i^i Fin ) C_ A ) )
13 8 10 12 3imtr4d 
 |-  ( ( ph /\ D C_ C ) -> ( C e. A -> D e. A ) )
14 13 impancom 
 |-  ( ( ph /\ C e. A ) -> ( D C_ C -> D e. A ) )
15 14 impr 
 |-  ( ( ph /\ ( C e. A /\ D C_ C ) ) -> D e. A )