Metamath Proof Explorer

Theorem mnuop123d

Description: Operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

		Ref	Expression
	Hypotheses	mnuop123d.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 ) ) ) ) }
		mnuop123d.2	\|- ( ph -> U e. M )
		mnuop123d.3	\|- ( ph -> A e. U )
	Assertion	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 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mnuop123d.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		mnuop123d.2	\|- ( ph -> U e. M )
3		mnuop123d.3	\|- ( ph -> A e. U )
4		pweq	\|- ( z = A -> ~P z = ~P A )
5	4	sseq1d	\|- ( z = A -> ( ~P z C_ U <-> ~P A C_ U ) )
6	4	sseq1d	\|- ( z = A -> ( ~P z C_ w <-> ~P A C_ w ) )
7		raleq	\|- ( z = A -> ( A. i e. z ( 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 ) ) ) )
8	6 7	anbi12d	\|- ( z = A -> ( ( ~P z C_ w /\ A. i e. z ( 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 ) ) ) ) )
9	8	rexbidv	\|- ( z = A -> ( E. w e. U ( ~P z C_ w /\ A. i e. z ( 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 ) ) ) ) )
10	9	albidv	\|- ( z = A -> ( A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) <-> 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 ) ) ) ) )
11	5 10	anbi12d	\|- ( z = A -> ( ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) <-> ( ~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 ) ) ) ) ) )
12	1	ismnu	\|- ( U e. M -> ( U e. M <-> A. z e. U ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) ) )
13	12	ibi	\|- ( U e. M -> A. z e. U ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
14	2 13	syl	\|- ( ph -> A. z e. U ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
15	11 14 3	rspcdva	\|- ( 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 ) ) ) ) )