Theorem mnurnd

Description: Minimal universes contain ranges of functions from an element of the universe to the universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypotheses	mnurnd.1	|- M = { 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 ) ) ) ) }
	mnurnd.2	|- ( ph -> U e. M )
	mnurnd.3	|- ( ph -> A e. U )
	mnurnd.4	|- ( ph -> F : A --> U )
Assertion	mnurnd	|- ( ph -> ran F e. U )

Proof

Step	Hyp	Ref	Expression
1		mnurnd.1	|- M = { 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		mnurnd.2	|- ( ph -> U e. M )
3		mnurnd.3	|- ( ph -> A e. U )
4		mnurnd.4	|- ( ph -> F : A --> U )
5	3	elexd	|- ( ph -> A e. _V )
6	5	iftrued	|- ( ph -> if ( A e. _V , A , (/) ) = A )
7	6 3	eqeltrd	|- ( ph -> if ( A e. _V , A , (/) ) e. U )
8	6	feq2d	|- ( ph -> ( F : if ( A e. _V , A , (/) ) --> U <-> F : A --> U ) )
9	4 8	mpbird	|- ( ph -> F : if ( A e. _V , A , (/) ) --> U )
10		0ex	|- (/) e. _V
11	10	elimel	|- if ( A e. _V , A , (/) ) e. _V
12	1 2 7 9 11	mnurndlem2	|- ( ph -> ran F e. U )