Metamath Proof Explorer


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