Metamath Proof Explorer

Theorem iswun

Description: Properties of a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion iswun 
|- ( U e. V -> ( 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 treq 
 |-  ( u = U -> ( Tr u <-> Tr U ) )
2 neeq1 
 |-  ( u = U -> ( u =/= (/) <-> U =/= (/) ) )
3 eleq2 
 |-  ( u = U -> ( U. x e. u <-> U. x e. U ) )
4 eleq2 
 |-  ( u = U -> ( ~P x e. u <-> ~P x e. U ) )
5 eleq2 
 |-  ( u = U -> ( { x , y } e. u <-> { x , y } e. U ) )
6 5 raleqbi1dv 
 |-  ( u = U -> ( A. y e. u { x , y } e. u <-> A. y e. U { x , y } e. U ) )
7 3 4 6 3anbi123d 
 |-  ( u = U -> ( ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) <-> ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) )
8 7 raleqbi1dv 
 |-  ( u = U -> ( A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) <-> A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) )
9 1 2 8 3anbi123d 
 |-  ( u = U -> ( ( Tr u /\ u =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) ) <-> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) ) )
10 df-wun 
 |-  WUni = { u | ( Tr u /\ u =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) ) }
11 9 10 elab2g 
 |-  ( U e. V -> ( 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 ) ) ) )