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 | |
|
hsmexlem.g | |
||
Assertion | hsmexlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hsmexlem.f | |
|
2 | hsmexlem.g | |
|
3 | elpwi | |
|
4 | 3 | adantr | |
5 | 4 | ralimi | |
6 | iunss | |
|
7 | 5 6 | sylibr | |
8 | 7 | 3ad2ant3 | |
9 | xpexg | |
|
10 | 9 | 3adant3 | |
11 | nfv | |
|
12 | nfra1 | |
|
13 | 11 12 | nfan | |
14 | rsp | |
|
15 | onelss | |
|
16 | 15 | imp | |
17 | 16 | adantrl | |
18 | 17 | 3adant3 | |
19 | 1 | oismo | |
20 | 3 19 | syl | |
21 | 20 | ad2antrl | |
22 | 21 | simprd | |
23 | 1 | oif | |
24 | 22 23 | jctil | |
25 | dffo2 | |
|
26 | 24 25 | sylibr | |
27 | dffo3 | |
|
28 | 27 | simprbi | |
29 | rsp | |
|
30 | 26 28 29 | 3syl | |
31 | 30 | 3impia | |
32 | ssrexv | |
|
33 | 18 31 32 | sylc | |
34 | 33 | 3exp | |
35 | 14 34 | sylan9r | |
36 | 13 35 | reximdai | |
37 | 36 | 3adant1 | |
38 | nfv | |
|
39 | nfcv | |
|
40 | nfcv | |
|
41 | nfcsb1v | |
|
42 | 40 41 | nfoi | |
43 | nfcv | |
|
44 | 42 43 | nffv | |
45 | 44 | nfeq2 | |
46 | 39 45 | nfrexw | |
47 | csbeq1a | |
|
48 | oieq2 | |
|
49 | 47 48 | syl | |
50 | 1 49 | eqtrid | |
51 | 50 | fveq1d | |
52 | 51 | eqeq2d | |
53 | 52 | rexbidv | |
54 | 38 46 53 | cbvrexw | |
55 | 37 54 | imbitrdi | |
56 | eliun | |
|
57 | vex | |
|
58 | vex | |
|
59 | 57 58 | op1std | |
60 | 59 | csbeq1d | |
61 | oieq2 | |
|
62 | 60 61 | syl | |
63 | 57 58 | op2ndd | |
64 | 62 63 | fveq12d | |
65 | 64 | eqeq2d | |
66 | 65 | rexxp | |
67 | 55 56 66 | 3imtr4g | |
68 | 67 | imp | |
69 | 10 68 | wdomd | |
70 | 2 | hsmexlem1 | |
71 | 8 69 70 | syl2anc | |