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 )