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 ⊢φ→F:card⁡⋃A∖B⟶1-1 onto⋃A∖B
ttukeylem.2 ⊢φ→B∈A
ttukeylem.3 ⊢φ→∀xx∈A↔𝒫x∩Fin⊆A
Assertion ttukeylem2 ⊢φ∧C∈A∧D⊆C→D∈A

Proof

Step Hyp Ref Expression
1 ttukeylem.1 ⊢φ→F:card⁡⋃A∖B⟶1-1 onto⋃A∖B
2 ttukeylem.2 ⊢φ→B∈A
3 ttukeylem.3 ⊢φ→∀xx∈A↔𝒫x∩Fin⊆A
4 simpr ⊢φ∧D⊆C→D⊆C
5 4 sspwd ⊢φ∧D⊆C→𝒫D⊆𝒫C
6 ssrin ⊢𝒫D⊆𝒫C→𝒫D∩Fin⊆𝒫C∩Fin
7 sstr2 ⊢𝒫D∩Fin⊆𝒫C∩Fin→𝒫C∩Fin⊆A→𝒫D∩Fin⊆A
8 5 6 7 3syl ⊢φ∧D⊆C→𝒫C∩Fin⊆A→𝒫D∩Fin⊆A
9 1 2 3 ttukeylem1 ⊢φ→C∈A↔𝒫C∩Fin⊆A
10 9 adantr ⊢φ∧D⊆C→C∈A↔𝒫C∩Fin⊆A
11 1 2 3 ttukeylem1 ⊢φ→D∈A↔𝒫D∩Fin⊆A
12 11 adantr ⊢φ∧D⊆C→D∈A↔𝒫D∩Fin⊆A
13 8 10 12 3imtr4d ⊢φ∧D⊆C→C∈A→D∈A
14 13 impancom ⊢φ∧C∈A→D⊆C→D∈A
15 14 impr ⊢φ∧C∈A∧D⊆C→D∈A