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 )