Theorem winafpi

Description: This theorem, which states that a nontrivial inaccessible cardinal is its own aleph number, is stated here in inference form, where the assumptions are in the hypotheses rather than an antecedent. Often, we use dedth to turn this type of statement into the closed form statement winafp , but in this case, since it is consistent with ZFC that there are no nontrivial inaccessible cardinals, it is not possible to prove winafp using this theorem and dedth , in ZFC. (You can prove this if you use ax-groth , though.) (Contributed by Mario Carneiro, 28-May-2014)

	Ref	Expression
Hypotheses	winafp.1	|- A e. InaccW
	winafp.2	|- A =/= _om
Assertion	winafpi	|- ( aleph ` A ) = A

Proof

Step	Hyp	Ref	Expression
1		winafp.1	|- A e. InaccW
2		winafp.2	|- A =/= _om
3		winafp	|- ( ( A e. InaccW /\ A =/= _om ) -> ( aleph ` A ) = A )
4	1 2 3	mp2an	|- ( aleph ` A ) = A