Theorem mnuop23d

Description: Second and third operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypotheses	mnuop23d.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 ) ) ) ) }
	mnuop23d.2	|- ( ph -> U e. M )
	mnuop23d.3	|- ( ph -> A e. U )
	mnuop23d.4	|- ( ph -> F e. V )
Assertion	mnuop23d	|- ( ph -> E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. F ) -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mnuop23d.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		mnuop23d.2	|- ( ph -> U e. M )
3		mnuop23d.3	|- ( ph -> A e. U )
4		mnuop23d.4	|- ( ph -> F e. V )
5	1 2 3	mnuop123d	|- ( ph -> ( ~P A C_ U /\ A. f E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
6	5	simprd	|- ( ph -> A. f E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) )
7		eleq2	|- ( f = F -> ( v e. f <-> v e. F ) )
8	7	anbi2d	|- ( f = F -> ( ( i e. v /\ v e. f ) <-> ( i e. v /\ v e. F ) ) )
9	8	rexbidv	|- ( f = F -> ( E. v e. U ( i e. v /\ v e. f ) <-> E. v e. U ( i e. v /\ v e. F ) ) )
10		rexeq	|- ( f = F -> ( E. u e. f ( i e. u /\ U. u C_ w ) <-> E. u e. F ( i e. u /\ U. u C_ w ) ) )
11	9 10	imbi12d	|- ( f = F -> ( ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) <-> ( E. v e. U ( i e. v /\ v e. F ) -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) )
12	11	ralbidv	|- ( f = F -> ( A. i e. A ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) <-> A. i e. A ( E. v e. U ( i e. v /\ v e. F ) -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) )
13	12	anbi2d	|- ( f = F -> ( ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) <-> ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. F ) -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) )
14	13	rexbidv	|- ( f = F -> ( E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) <-> E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. F ) -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) )
15	14	spcgv	|- ( F e. V -> ( A. f E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) -> E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. F ) -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) )
16	4 6 15	sylc	|- ( ph -> E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. F ) -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) )