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	⊢ ( 𝜑 → ¬ 𝐵 ≼ ω )