Metamath Proof Explorer


Theorem hsmexlem2

Description: Lemma for hsmex . Bound the order type of a union of sets of ordinals, each of limited order type. Vaguely reminiscent of unictb but use of order types allows to canonically choose the sub-bijections, removing the choice requirement. (Contributed by Stefan O'Rear, 14-Feb-2015) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by AV, 18-Sep-2021)

Ref Expression
Hypotheses hsmexlem.f F=OrdIsoEB
hsmexlem.g G=OrdIsoEaAB
Assertion hsmexlem2 AVCOnaAB𝒫OndomFCdomGhar𝒫A×C

Proof

Step Hyp Ref Expression
1 hsmexlem.f F=OrdIsoEB
2 hsmexlem.g G=OrdIsoEaAB
3 elpwi B𝒫OnBOn
4 3 adantr B𝒫OndomFCBOn
5 4 ralimi aAB𝒫OndomFCaABOn
6 iunss aABOnaABOn
7 5 6 sylibr aAB𝒫OndomFCaABOn
8 7 3ad2ant3 AVCOnaAB𝒫OndomFCaABOn
9 xpexg AVCOnA×CV
10 9 3adant3 AVCOnaAB𝒫OndomFCA×CV
11 nfv aCOn
12 nfra1 aaAB𝒫OndomFC
13 11 12 nfan aCOnaAB𝒫OndomFC
14 rsp aAB𝒫OndomFCaAB𝒫OndomFC
15 onelss COndomFCdomFC
16 15 imp COndomFCdomFC
17 16 adantrl COnB𝒫OndomFCdomFC
18 17 3adant3 COnB𝒫OndomFCbBdomFC
19 1 oismo BOnSmoFranF=B
20 3 19 syl B𝒫OnSmoFranF=B
21 20 ad2antrl COnB𝒫OndomFCSmoFranF=B
22 21 simprd COnB𝒫OndomFCranF=B
23 1 oif F:domFB
24 22 23 jctil COnB𝒫OndomFCF:domFBranF=B
25 dffo2 F:domFontoBF:domFBranF=B
26 24 25 sylibr COnB𝒫OndomFCF:domFontoB
27 dffo3 F:domFontoBF:domFBbBedomFb=Fe
28 27 simprbi F:domFontoBbBedomFb=Fe
29 rsp bBedomFb=FebBedomFb=Fe
30 26 28 29 3syl COnB𝒫OndomFCbBedomFb=Fe
31 30 3impia COnB𝒫OndomFCbBedomFb=Fe
32 ssrexv domFCedomFb=FeeCb=Fe
33 18 31 32 sylc COnB𝒫OndomFCbBeCb=Fe
34 33 3exp COnB𝒫OndomFCbBeCb=Fe
35 14 34 sylan9r COnaAB𝒫OndomFCaAbBeCb=Fe
36 13 35 reximdai COnaAB𝒫OndomFCaAbBaAeCb=Fe
37 36 3adant1 AVCOnaAB𝒫OndomFCaAbBaAeCb=Fe
38 nfv deCb=Fe
39 nfcv _aC
40 nfcv _aE
41 nfcsb1v _ad/aB
42 40 41 nfoi _aOrdIsoEd/aB
43 nfcv _ae
44 42 43 nffv _aOrdIsoEd/aBe
45 44 nfeq2 ab=OrdIsoEd/aBe
46 39 45 nfrexw aeCb=OrdIsoEd/aBe
47 csbeq1a a=dB=d/aB
48 oieq2 B=d/aBOrdIsoEB=OrdIsoEd/aB
49 47 48 syl a=dOrdIsoEB=OrdIsoEd/aB
50 1 49 eqtrid a=dF=OrdIsoEd/aB
51 50 fveq1d a=dFe=OrdIsoEd/aBe
52 51 eqeq2d a=db=Feb=OrdIsoEd/aBe
53 52 rexbidv a=deCb=FeeCb=OrdIsoEd/aBe
54 38 46 53 cbvrexw aAeCb=FedAeCb=OrdIsoEd/aBe
55 37 54 imbitrdi AVCOnaAB𝒫OndomFCaAbBdAeCb=OrdIsoEd/aBe
56 eliun baABaAbB
57 vex dV
58 vex eV
59 57 58 op1std c=de1stc=d
60 59 csbeq1d c=de1stc/aB=d/aB
61 oieq2 1stc/aB=d/aBOrdIsoE1stc/aB=OrdIsoEd/aB
62 60 61 syl c=deOrdIsoE1stc/aB=OrdIsoEd/aB
63 57 58 op2ndd c=de2ndc=e
64 62 63 fveq12d c=deOrdIsoE1stc/aB2ndc=OrdIsoEd/aBe
65 64 eqeq2d c=deb=OrdIsoE1stc/aB2ndcb=OrdIsoEd/aBe
66 65 rexxp cA×Cb=OrdIsoE1stc/aB2ndcdAeCb=OrdIsoEd/aBe
67 55 56 66 3imtr4g AVCOnaAB𝒫OndomFCbaABcA×Cb=OrdIsoE1stc/aB2ndc
68 67 imp AVCOnaAB𝒫OndomFCbaABcA×Cb=OrdIsoE1stc/aB2ndc
69 10 68 wdomd AVCOnaAB𝒫OndomFCaAB*A×C
70 2 hsmexlem1 aABOnaAB*A×CdomGhar𝒫A×C
71 8 69 70 syl2anc AVCOnaAB𝒫OndomFCdomGhar𝒫A×C