Theorem rr-grothshortbi

Description: Express "every set is contained in a Grothendieck universe" in a short form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 8-Oct-2024)

	Ref	Expression
Assertion	rr-grothshortbi	|- ( A. x E. y e. Univ x e. y <-> A. x E. y ( x e. 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		df-rex	|- ( E. y e. Univ x e. y <-> E. y ( y e. Univ /\ x e. y ) )
2		exancom	|- ( E. y ( y e. Univ /\ x e. y ) <-> E. y ( x e. y /\ y e. Univ ) )
3		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 ) ) }
4	3	abeq2i	|- ( 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 ) ) )
5	4	anbi2i	|- ( ( x e. y /\ y e. Univ ) <-> ( x e. 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 ) ) ) )
6	5	exbii	|- ( E. y ( x e. y /\ y e. Univ ) <-> E. y ( x e. 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 ) ) ) )
7	1 2 6	3bitri	|- ( E. y e. Univ x e. y <-> E. y ( x e. 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 ) ) ) )
8	7	albii	|- ( A. x E. y e. Univ x e. y <-> A. x E. y ( x e. 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 ) ) ) )