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 ⊢ ( 𝜑 → ¬ 𝐴 ≼ ω )
ssnct.2 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion ssnct ( 𝜑 → ¬ 𝐵 ≼ ω )

Proof

Step Hyp Ref Expression
1 ssnct.1 ⊢ ( 𝜑 → ¬ 𝐴 ≼ ω )
2 ssnct.2 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
3 ssct ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω ) → 𝐴 ≼ ω )
4 2 3 sylan ⊢ ( ( 𝜑 ∧ 𝐵 ≼ ω ) → 𝐴 ≼ ω )
5 1 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≼ ω ) → ¬ 𝐴 ≼ ω )
6 4 5 pm2.65da ⊢ ( 𝜑 → ¬ 𝐵 ≼ ω )