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	⊢ ( 𝜑 → 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
	ttukeylem.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
	ttukeylem.3	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) )
Assertion	ttukeylem2	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ⊆ 𝐶 ) ) → 𝐷 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ttukeylem.1	⊢ ( 𝜑 → 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
2		ttukeylem.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3		ttukeylem.3	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) )
4		simpr	⊢ ( ( 𝜑 ∧ 𝐷 ⊆ 𝐶 ) → 𝐷 ⊆ 𝐶 )
5	4	sspwd	⊢ ( ( 𝜑 ∧ 𝐷 ⊆ 𝐶 ) → 𝒫 𝐷 ⊆ 𝒫 𝐶 )
6		ssrin	⊢ ( 𝒫 𝐷 ⊆ 𝒫 𝐶 → ( 𝒫 𝐷 ∩ Fin ) ⊆ ( 𝒫 𝐶 ∩ Fin ) )
7		sstr2	⊢ ( ( 𝒫 𝐷 ∩ Fin ) ⊆ ( 𝒫 𝐶 ∩ Fin ) → ( ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 → ( 𝒫 𝐷 ∩ Fin ) ⊆ 𝐴 ) )
8	5 6 7	3syl	⊢ ( ( 𝜑 ∧ 𝐷 ⊆ 𝐶 ) → ( ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 → ( 𝒫 𝐷 ∩ Fin ) ⊆ 𝐴 ) )
9	1 2 3	ttukeylem1	⊢ ( 𝜑 → ( 𝐶 ∈ 𝐴 ↔ ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 ) )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ⊆ 𝐶 ) → ( 𝐶 ∈ 𝐴 ↔ ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 ) )
11	1 2 3	ttukeylem1	⊢ ( 𝜑 → ( 𝐷 ∈ 𝐴 ↔ ( 𝒫 𝐷 ∩ Fin ) ⊆ 𝐴 ) )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ⊆ 𝐶 ) → ( 𝐷 ∈ 𝐴 ↔ ( 𝒫 𝐷 ∩ Fin ) ⊆ 𝐴 ) )
13	8 10 12	3imtr4d	⊢ ( ( 𝜑 ∧ 𝐷 ⊆ 𝐶 ) → ( 𝐶 ∈ 𝐴 → 𝐷 ∈ 𝐴 ) )
14	13	impancom	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐷 ⊆ 𝐶 → 𝐷 ∈ 𝐴 ) )
15	14	impr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ⊆ 𝐶 ) ) → 𝐷 ∈ 𝐴 )