Metamath Proof Explorer


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 BOnABMAMB

Proof

Step Hyp Ref Expression
1 imass2 ABMAMB
2 1 unissd ABMAMB
3 2 sspwd AB𝒫MA𝒫MB
4 3 adantl BOnAB𝒫MA𝒫MB
5 4 adantl AOnBOnAB𝒫MA𝒫MB
6 ssrexv 𝒫MA𝒫MBa𝒫MAb𝒫MAasba|sb=xa𝒫MBb𝒫MAasba|sb=x
7 5 6 syl AOnBOnABa𝒫MAb𝒫MAasba|sb=xa𝒫MBb𝒫MAasba|sb=x
8 ssrexv 𝒫MA𝒫MBb𝒫MAasba|sb=xb𝒫MBasba|sb=x
9 5 8 syl AOnBOnABb𝒫MAasba|sb=xb𝒫MBasba|sb=x
10 9 reximdv AOnBOnABa𝒫MBb𝒫MAasba|sb=xa𝒫MBb𝒫MBasba|sb=x
11 7 10 syld AOnBOnABa𝒫MAb𝒫MAasba|sb=xa𝒫MBb𝒫MBasba|sb=x
12 11 adantr AOnBOnABxNoa𝒫MAb𝒫MAasba|sb=xa𝒫MBb𝒫MBasba|sb=x
13 12 ss2rabdv AOnBOnABxNo|a𝒫MAb𝒫MAasba|sb=xxNo|a𝒫MBb𝒫MBasba|sb=x
14 madeval2 AOnMA=xNo|a𝒫MAb𝒫MAasba|sb=x
15 14 adantr AOnBOnABMA=xNo|a𝒫MAb𝒫MAasba|sb=x
16 madeval2 BOnMB=xNo|a𝒫MBb𝒫MBasba|sb=x
17 16 adantr BOnABMB=xNo|a𝒫MBb𝒫MBasba|sb=x
18 17 adantl AOnBOnABMB=xNo|a𝒫MBb𝒫MBasba|sb=x
19 13 15 18 3sstr4d AOnBOnABMAMB
20 madef M:On𝒫No
21 20 fdmi domM=On
22 21 eleq2i AdomMAOn
23 ndmfv ¬AdomMMA=
24 22 23 sylnbir ¬AOnMA=
25 0ss MB
26 24 25 eqsstrdi ¬AOnMAMB
27 26 adantr ¬AOnBOnABMAMB
28 19 27 pm2.61ian BOnABMAMB