Theorem madess

Description: If 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, 9-Oct-2024)

	Ref	Expression
Assertion	madess	|- ( ( 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	unissd	|- ( A C_ B -> U. ( _M " A ) C_ U. ( _M " B ) )
3	2	sspwd	|- ( A C_ B -> ~P U. ( _M " A ) C_ ~P U. ( _M " B ) )
4	3	adantl	|- ( ( B e. On /\ A C_ B ) -> ~P U. ( _M " A ) C_ ~P U. ( _M " B ) )
5	4	adantl	|- ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ~P U. ( _M " A ) C_ ~P U. ( _M " B ) )
6		ssrexv	|- ( ~P U. ( _M " A ) C_ ~P U. ( _M " B ) -> ( E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a < E. a e. ~P U. ( _M " B ) E. b e. ~P U. ( _M " A ) ( a <
7	5 6	syl	|- ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a < E. a e. ~P U. ( _M " B ) E. b e. ~P U. ( _M " A ) ( a <
8		ssrexv	|- ( ~P U. ( _M " A ) C_ ~P U. ( _M " B ) -> ( E. b e. ~P U. ( _M " A ) ( a < E. b e. ~P U. ( _M " B ) ( a <
9	5 8	syl	|- ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( E. b e. ~P U. ( _M " A ) ( a < E. b e. ~P U. ( _M " B ) ( a <
10	9	reximdv	|- ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( E. a e. ~P U. ( _M " B ) E. b e. ~P U. ( _M " A ) ( a < E. a e. ~P U. ( _M " B ) E. b e. ~P U. ( _M " B ) ( a <
11	7 10	syld	|- ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a < E. a e. ~P U. ( _M " B ) E. b e. ~P U. ( _M " B ) ( a <
12	11	adantr	|- ( ( ( A e. On /\ ( B e. On /\ A C_ B ) ) /\ x e. No ) -> ( E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a < E. a e. ~P U. ( _M " B ) E. b e. ~P U. ( _M " B ) ( a <
13	12	ss2rabdv	|- ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> { x e. No | E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a <
14		madeval2	|- ( A e. On -> ( _M ` A ) = { x e. No | E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a <
15	14	adantr	|- ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( _M ` A ) = { x e. No | E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a <
16		madeval2	|- ( B e. On -> ( _M ` B ) = { x e. No | E. a e. ~P U. ( _M " B ) E. b e. ~P U. ( _M " B ) ( a <
17	16	adantr	|- ( ( B e. On /\ A C_ B ) -> ( _M ` B ) = { x e. No | E. a e. ~P U. ( _M " B ) E. b e. ~P U. ( _M " B ) ( a <
18	17	adantl	|- ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( _M ` B ) = { x e. No | E. a e. ~P U. ( _M " B ) E. b e. ~P U. ( _M " B ) ( a <
19	13 15 18	3sstr4d	|- ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( _M ` A ) C_ ( _M ` B ) )
20		madef	|- _M : On --> ~P No
21	20	fdmi	|- dom _M = On
22	21	eleq2i	|- ( A e. dom _M <-> A e. On )
23		ndmfv	|- ( -. A e. dom _M -> ( _M ` A ) = (/) )
24	22 23	sylnbir	|- ( -. A e. On -> ( _M ` A ) = (/) )
25		0ss	|- (/) C_ ( _M ` B )
26	24 25	eqsstrdi	|- ( -. A e. On -> ( _M ` A ) C_ ( _M ` B ) )
27	26	adantr	|- ( ( -. A e. On /\ ( B e. On /\ A C_ B ) ) -> ( _M ` A ) C_ ( _M ` B ) )
28	19 27	pm2.61ian	|- ( ( B e. On /\ A C_ B ) -> ( _M ` A ) C_ ( _M ` B ) )