Theorem ssnct

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

	Ref	Expression
Hypotheses	ssnct.1	$$⊢\phi \to \neg A\preccurlyeq \mathrm{\omega }$$
	ssnct.2	$$⊢\phi \to A\subseteq B$$
Assertion	ssnct	$$⊢\phi \to \neg B\preccurlyeq \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		ssnct.1	$$⊢\phi \to \neg A\preccurlyeq \mathrm{\omega }$$
2		ssnct.2	$$⊢\phi \to A\subseteq B$$
3		ssct	$$⊢\left(A\subseteq B\wedge B\preccurlyeq \mathrm{\omega }\right)\to A\preccurlyeq \mathrm{\omega }$$
4	2 3	sylan	$$⊢\left(\phi \wedge B\preccurlyeq \mathrm{\omega }\right)\to A\preccurlyeq \mathrm{\omega }$$
5	1	adantr	$$⊢\left(\phi \wedge B\preccurlyeq \mathrm{\omega }\right)\to \neg A\preccurlyeq \mathrm{\omega }$$
6	4 5	pm2.65da	$$⊢\phi \to \neg B\preccurlyeq \mathrm{\omega }$$