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 ⊢ ( 𝜑 → 𝐹 : ( 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 ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ⊆ 𝐶 ) ) → 𝐷 ∈ 𝐴 )