Theorem mnurndlem2

Description: Lemma for mnurnd . Deduction theorem input. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypotheses	mnurndlem2.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 ) ) ) ) }
	mnurndlem2.2	|- ( ph -> U e. M )
	mnurndlem2.3	|- ( ph -> A e. U )
	mnurndlem2.4	|- ( ph -> F : A --> U )
	mnurndlem2.5	|- A e. _V
Assertion	mnurndlem2	|- ( ph -> ran F e. U )

Proof

Step	Hyp	Ref	Expression
1		mnurndlem2.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		mnurndlem2.2	|- ( ph -> U e. M )
3		mnurndlem2.3	|- ( ph -> A e. U )
4		mnurndlem2.4	|- ( ph -> F : A --> U )
5		mnurndlem2.5	|- A e. _V
6	2	adantr	|- ( ( ph /\ a e. A ) -> U e. M )
7	3	adantr	|- ( ( ph /\ a e. A ) -> A e. U )
8		simpr	|- ( ( ph /\ a e. A ) -> a e. A )
9	1 6 7 8	mnutrcld	|- ( ( ph /\ a e. A ) -> a e. U )
10	4	ffvelrnda	|- ( ( ph /\ a e. A ) -> ( F ` a ) e. U )
11	1 6 10 7	mnuprd	|- ( ( ph /\ a e. A ) -> { ( F ` a ) , A } e. U )
12	1 6 9 11	mnuprd	|- ( ( ph /\ a e. A ) -> { a , { ( F ` a ) , A } } e. U )
13	12	ralrimiva	|- ( ph -> A. a e. A { a , { ( F ` a ) , A } } e. U )
14		eqid	|- ( a e. A |-> { a , { ( F ` a ) , A } } ) = ( a e. A |-> { a , { ( F ` a ) , A } } )
15	14	rnmptss	|- ( A. a e. A { a , { ( F ` a ) , A } } e. U -> ran ( a e. A |-> { a , { ( F ` a ) , A } } ) C_ U )
16	13 15	syl	|- ( ph -> ran ( a e. A |-> { a , { ( F ` a ) , A } } ) C_ U )
17	1 2 3 16	mnuop3d	|- ( ph -> E. w e. U A. i e. A ( E. v e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) i e. v -> E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) ) )
18		simprl	|- ( ( ph /\ ( w e. U /\ A. i e. A ( E. v e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) i e. v -> E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) ) ) ) -> w e. U )
19		sseq2	|- ( b = w -> ( ran F C_ b <-> ran F C_ w ) )
20	19	adantl	|- ( ( ( ph /\ ( w e. U /\ A. i e. A ( E. v e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) i e. v -> E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) ) ) ) /\ b = w ) -> ( ran F C_ b <-> ran F C_ w ) )
21	4	adantr	|- ( ( ph /\ ( w e. U /\ A. i e. A ( E. v e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) i e. v -> E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) ) ) ) -> F : A --> U )
22		simprr	|- ( ( ph /\ ( w e. U /\ A. i e. A ( E. v e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) i e. v -> E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) ) ) ) -> A. i e. A ( E. v e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) i e. v -> E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) ) )
23	21 5 22	mnurndlem1	|- ( ( ph /\ ( w e. U /\ A. i e. A ( E. v e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) i e. v -> E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) ) ) ) -> ran F C_ w )
24	18 20 23	rspcedvd	|- ( ( ph /\ ( w e. U /\ A. i e. A ( E. v e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) i e. v -> E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) ) ) ) -> E. b e. U ran F C_ b )
25	17 24	rexlimddv	|- ( ph -> E. b e. U ran F C_ b )
26	1 2 25	mnuss2d	|- ( ph -> ran F e. U )