Kunen's inconsistency axiom-free proof on Metamath

[Thierry Arnoux]

Hi all,

I noticed an interesting question about Metamath on ProofAssistants
StackExchange:

https://proofassistants.stackexchange.com/questions/1273/kunens-inconsistency-axiom-free-proof-on-metamath

The question says "Metamath", but what is meant is really "set.mm". I
have tried to answer some general Metamath related questions there in
the past, but this is beyond my capabilities.

Kunen's original paper is not freely accessible, but a proof of his
theorem is present as theorem 1.12, page 10 of the PDF:

http://math.bu.edu/people/aki/d.pdf

I believe the first difficulty will be to express things like "inner
model" and "elementary embedding" in set.mm.

I'm reposting here in case anyone may be interested.

BR,
_
Thierry