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 ⊢ φ → ∀ x x ∈ 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 ⊢ φ → ∀ x x ∈ 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