Theorem madess

Description: If ordinal A is less than or equal to ordinal B , then the made set of A is included in the made set of B . (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	madess	|- ( ( A e. On /\ B e. On /\ A C_ B ) -> ( _M ` A ) C_ ( _M ` B ) )

Proof

Step	Hyp	Ref	Expression
1		imass2	|- ( A C_ B -> ( _M " A ) C_ ( _M " B ) )
2	1	3ad2ant3	|- ( ( A e. On /\ B e. On /\ A C_ B ) -> ( _M " A ) C_ ( _M " B ) )
3	2	adantr	|- ( ( ( A e. On /\ B e. On /\ A C_ B ) /\ x e. No ) -> ( _M " A ) C_ ( _M " B ) )
4	3	unissd	|- ( ( ( A e. On /\ B e. On /\ A C_ B ) /\ x e. No ) -> U. ( _M " A ) C_ U. ( _M " B ) )
5	4	sspwd	|- ( ( ( A e. On /\ B e. On /\ A C_ B ) /\ x e. No ) -> ~P U. ( _M " A ) C_ ~P U. ( _M " B ) )
6		ssrexv	|- ( ~P U. ( _M " A ) C_ ~P U. ( _M " B ) -> ( E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l < E. l e. ~P U. ( _M " B ) E. r e. ~P U. ( _M " A ) ( l <
7	5 6	syl	|- ( ( ( A e. On /\ B e. On /\ A C_ B ) /\ x e. No ) -> ( E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l < E. l e. ~P U. ( _M " B ) E. r e. ~P U. ( _M " A ) ( l <
8		ssrexv	|- ( ~P U. ( _M " A ) C_ ~P U. ( _M " B ) -> ( E. r e. ~P U. ( _M " A ) ( l < E. r e. ~P U. ( _M " B ) ( l <
9	5 8	syl	|- ( ( ( A e. On /\ B e. On /\ A C_ B ) /\ x e. No ) -> ( E. r e. ~P U. ( _M " A ) ( l < E. r e. ~P U. ( _M " B ) ( l <
10	9	reximdv	|- ( ( ( A e. On /\ B e. On /\ A C_ B ) /\ x e. No ) -> ( E. l e. ~P U. ( _M " B ) E. r e. ~P U. ( _M " A ) ( l < E. l e. ~P U. ( _M " B ) E. r e. ~P U. ( _M " B ) ( l <
11	7 10	syld	|- ( ( ( A e. On /\ B e. On /\ A C_ B ) /\ x e. No ) -> ( E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l < E. l e. ~P U. ( _M " B ) E. r e. ~P U. ( _M " B ) ( l <
12	11	ralrimiva	|- ( ( A e. On /\ B e. On /\ A C_ B ) -> A. x e. No ( E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l < E. l e. ~P U. ( _M " B ) E. r e. ~P U. ( _M " B ) ( l <
13		ss2rab	|- ( { x e. No | E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l < A. x e. No ( E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l < E. l e. ~P U. ( _M " B ) E. r e. ~P U. ( _M " B ) ( l <
14	12 13	sylibr	|- ( ( A e. On /\ B e. On /\ A C_ B ) -> { x e. No | E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l <
15		madeval2	|- ( A e. On -> ( _M ` A ) = { x e. No | E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l <
16	15	3ad2ant1	|- ( ( A e. On /\ B e. On /\ A C_ B ) -> ( _M ` A ) = { x e. No | E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l <
17		madeval2	|- ( B e. On -> ( _M ` B ) = { x e. No | E. l e. ~P U. ( _M " B ) E. r e. ~P U. ( _M " B ) ( l <
18	17	3ad2ant2	|- ( ( A e. On /\ B e. On /\ A C_ B ) -> ( _M ` B ) = { x e. No | E. l e. ~P U. ( _M " B ) E. r e. ~P U. ( _M " B ) ( l <
19	14 16 18	3sstr4d	|- ( ( A e. On /\ B e. On /\ A C_ B ) -> ( _M ` A ) C_ ( _M ` B ) )