This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wun0

Description: A weak universe contains the empty set. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypothesis wun0.1 
|- ( ph -> U e. WUni )
Assertion wun0 
|- ( ph -> (/) e. U )

Proof

Step Hyp Ref Expression
1 wun0.1 
 |-  ( ph -> U e. WUni )
2 iswun 
 |-  ( U e. WUni -> ( U e. WUni <-> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) ) )
3 2 ibi 
 |-  ( U e. WUni -> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) )
4 3 simp2d 
 |-  ( U e. WUni -> U =/= (/) )
5 1 4 syl 
 |-  ( ph -> U =/= (/) )
6 n0 
 |-  ( U =/= (/) <-> E. x x e. U )
7 5 6 sylib 
 |-  ( ph -> E. x x e. U )
8 1 adantr 
 |-  ( ( ph /\ x e. U ) -> U e. WUni )
9 simpr 
 |-  ( ( ph /\ x e. U ) -> x e. U )
10 0ss 
 |-  (/) C_ x
11 10 a1i 
 |-  ( ( ph /\ x e. U ) -> (/) C_ x )
12 8 9 11 wunss 
 |-  ( ( ph /\ x e. U ) -> (/) e. U )
13 7 12 exlimddv 
 |-  ( ph -> (/) e. U )