Theorem ssnct

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

	Ref	Expression
Hypotheses	ssnct.1	|- ( ph -> -. A ~<_ _om )
	ssnct.2	|- ( ph -> A C_ B )
Assertion	ssnct	|- ( ph -> -. B ~<_ _om )

Proof

Step	Hyp	Ref	Expression
1		ssnct.1	|- ( ph -> -. A ~<_ _om )
2		ssnct.2	|- ( ph -> A C_ B )
3		ssct	|- ( ( A C_ B /\ B ~<_ _om ) -> A ~<_ _om )
4	2 3	sylan	|- ( ( ph /\ B ~<_ _om ) -> A ~<_ _om )
5	1	adantr	|- ( ( ph /\ B ~<_ _om ) -> -. A ~<_ _om )
6	4 5	pm2.65da	|- ( ph -> -. B ~<_ _om )