This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssnct

Description: A set containing an uncountable set is itself uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses ssnct.1 ⊢ φ → ¬ A ≼ ω
ssnct.2 ⊢ φ → A ⊆ B
Assertion ssnct ⊢ φ → ¬ B ≼ ω

Proof

Step Hyp Ref Expression
1 ssnct.1 ⊢ φ → ¬ A ≼ ω
2 ssnct.2 ⊢ φ → A ⊆ B
3 ssct ⊢ A ⊆ B ∧ B ≼ ω → A ≼ ω
4 2 3 sylan ⊢ φ ∧ B ≼ ω → A ≼ ω
5 1 adantr ⊢ φ ∧ B ≼ ω → ¬ A ≼ ω
6 4 5 pm2.65da ⊢ φ → ¬ B ≼ ω