Theorem bj-pwcfsdom

Description: Remove hypothesis from pwcfsdom . Illustration of how to remove a "proof-facilitating hypothesis". (Can use it to shorten theorems using pwcfsdom .) (Contributed by BJ, 14-Sep-2019)

	Ref	Expression
Assertion	bj-pwcfsdom	|- ( aleph ` A ) ~< ( ( aleph ` A ) ^m ( cf ` ( aleph ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( y e. ( cf ` ( aleph ` A ) ) |-> ( har ` ( f ` y ) ) ) = ( y e. ( cf ` ( aleph ` A ) ) |-> ( har ` ( f ` y ) ) )
2	1	pwcfsdom	|- ( aleph ` A ) ~< ( ( aleph ` A ) ^m ( cf ` ( aleph ` A ) ) )