This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Union Hartogs function harndom
Description: The Hartogs number of a set does not inject into that set. (Contributed by Stefan O'Rear , 11-Feb-2015) (Revised by Mario Carneiro , 15-May-2015)
Ref
Expression
Assertion
harndom ⊢ ¬ ( har ‘ 𝑋 ) ≼ 𝑋
Proof
Step
Hyp
Ref
Expression
1
harcl ⊢ ( har ‘ 𝑋 ) ∈ On
2
1
onirri ⊢ ¬ ( har ‘ 𝑋 ) ∈ ( har ‘ 𝑋 )
3
elharval ⊢ ( ( har ‘ 𝑋 ) ∈ ( har ‘ 𝑋 ) ↔ ( ( har ‘ 𝑋 ) ∈ On ∧ ( har ‘ 𝑋 ) ≼ 𝑋 ) )
4
1 3
mpbiran ⊢ ( ( har ‘ 𝑋 ) ∈ ( har ‘ 𝑋 ) ↔ ( har ‘ 𝑋 ) ≼ 𝑋 )
5
2 4
mtbi ⊢ ¬ ( har ‘ 𝑋 ) ≼ 𝑋