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 
 |-  ( z = w -> ( Tr z <-> Tr w ) )
2 neeq1 
 |-  ( z = w -> ( z =/= (/) <-> w =/= (/) ) )
3 eleq2 
 |-  ( z = w -> ( U. x e. z <-> U. x e. w ) )
4 eleq2 
 |-  ( z = w -> ( ~P x e. z <-> ~P x e. w ) )
5 eleq2 
 |-  ( z = w -> ( { x , y } e. z <-> { x , y } e. w ) )
6 5 raleqbi1dv 
 |-  ( z = w -> ( A. y e. z { x , y } e. z <-> A. y e. w { x , y } e. w ) )
7 3 4 6 3anbi123d 
 |-  ( z = w -> ( ( U. x e. z /\ ~P x e. z /\ A. y e. z { x , y } e. z ) <-> ( U. x e. w /\ ~P x e. w /\ A. y e. w { x , y } e. w ) ) )
8 7 raleqbi1dv 
 |-  ( z = w -> ( A. x e. z ( U. x e. z /\ ~P x e. z /\ A. y e. z { x , y } e. z ) <-> A. x e. w ( U. x e. w /\ ~P x e. w /\ A. y e. w { x , y } e. w ) ) )
9 1 2 8 3anbi123d 
 |-  ( z = w -> ( ( Tr z /\ z =/= (/) /\ A. x e. z ( U. x e. z /\ ~P x e. z /\ A. y e. z { x , y } e. z ) ) <-> ( Tr w /\ w =/= (/) /\ A. x e. w ( U. x e. w /\ ~P x e. w /\ A. y e. w { x , y } e. w ) ) ) )
10 treq 
 |-  ( w = U -> ( Tr w <-> Tr U ) )
11 neeq1 
 |-  ( w = U -> ( w =/= (/) <-> U =/= (/) ) )
12 eleq2 
 |-  ( w = U -> ( U. x e. w <-> U. x e. U ) )
13 eleq2 
 |-  ( w = U -> ( ~P x e. w <-> ~P x e. U ) )
14 eleq2 
 |-  ( w = U -> ( { x , y } e. w <-> { x , y } e. U ) )
15 14 raleqbi1dv 
 |-  ( w = U -> ( A. y e. w { x , y } e. w <-> A. y e. U { x , y } e. U ) )
16 12 13 15 3anbi123d 
 |-  ( w = U -> ( ( U. x e. w /\ ~P x e. w /\ A. y e. w { x , y } e. w ) <-> ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) )
17 16 raleqbi1dv 
 |-  ( w = U -> ( A. x e. w ( U. x e. w /\ ~P x e. w /\ A. y e. w { x , y } e. w ) <-> A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) )
18 10 11 17 3anbi123d 
 |-  ( w = U -> ( ( Tr w /\ w =/= (/) /\ A. x e. w ( U. x e. w /\ ~P x e. w /\ A. y e. w { x , y } e. w ) ) <-> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) ) )
19 df-wun 
 |-  WUni = { z | ( Tr z /\ z =/= (/) /\ A. x e. z ( U. x e. z /\ ~P x e. z /\ A. y e. z { x , y } e. z ) ) }
20 9 18 19 elab2gw 
 |-  ( 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 ) ) ) )