Metamath Proof Explorer

Theorem axhilex-zf

Description: Derive Axiom ax-hilex from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008) (New usage is discouraged.)

Ref Expression
Hypotheses axhil.1 
|- U = <. <. +h , .h >. , normh >.
axhil.2 
|- U e. CHilOLD
Assertion axhilex-zf 
|- ~H e. _V

Proof

Step Hyp Ref Expression
1 axhil.1 
 |-  U = <. <. +h , .h >. , normh >.
2 axhil.2 
 |-  U e. CHilOLD
3 df-hba 
 |-  ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )
4 3 hlex 
 |-  ~H e. _V