Theorem dfuniv2

Description: Alternative definition of Univ using only simple defined symbols. (Contributed by Rohan Ridenour, 10-Oct-2024)

	Ref	Expression
Assertion	dfuniv2	|- Univ = { y | A. z e. y A. f e. ~P y E. w e. y ( ~P z C_ ( y i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) }

Proof

Step	Hyp	Ref	Expression
1		grumnueq	|- Univ = { k | A. l e. k ( ~P l C_ k /\ A. m E. n e. k ( ~P l C_ n /\ A. p e. l ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) ) ) }
2	1	ismnu	|- ( y e. _V -> ( y e. Univ <-> A. z e. y ( ~P z C_ y /\ A. f E. w e. y ( ~P z C_ w /\ A. i e. z ( E. v e. y ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) ) )
3	2	elv	|- ( y e. Univ <-> A. z e. y ( ~P z C_ y /\ A. f E. w e. y ( ~P z C_ w /\ A. i e. z ( E. v e. y ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
4		ismnushort	|- ( A. f e. ~P y E. w e. y ( ~P z C_ ( y i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) <-> ( ~P z C_ y /\ A. f E. w e. y ( ~P z C_ w /\ A. i e. z ( E. v e. y ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
5	4	ralbii	|- ( A. z e. y A. f e. ~P y E. w e. y ( ~P z C_ ( y i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) <-> A. z e. y ( ~P z C_ y /\ A. f E. w e. y ( ~P z C_ w /\ A. i e. z ( E. v e. y ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
6	3 5	bitr4i	|- ( y e. Univ <-> A. z e. y A. f e. ~P y E. w e. y ( ~P z C_ ( y i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) )
7	6	abbi2i	|- Univ = { y | A. z e. y A. f e. ~P y E. w e. y ( ~P z C_ ( y i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) }