Proof of Theorem hartogslem1
Step | Hyp | Ref
| Expression |
1 | | hartogslem.2 |
. . . . 5
OrdIso |
2 | 1 | dmeqi 5325 |
. . . 4
OrdIso |
3 | | dmopab 5335 |
. . . 4
OrdIso
OrdIso |
4 | 2, 3 | eqtri 2644 |
. . 3
OrdIso |
5 | | simp3 1063 |
. . . . . . . 8
|
6 | | simp1 1061 |
. . . . . . . . 9
|
7 | | xpss12 5225 |
. . . . . . . . 9
|
8 | 6, 6, 7 | syl2anc 693 |
. . . . . . . 8
|
9 | 5, 8 | sstrd 3613 |
. . . . . . 7
|
10 | | selpw 4165 |
. . . . . . 7
|
11 | 9, 10 | sylibr 224 |
. . . . . 6
|
12 | 11 | ad2antrr 762 |
. . . . 5
OrdIso
|
13 | 12 | exlimiv 1858 |
. . . 4
OrdIso
|
14 | 13 | abssi 3677 |
. . 3
OrdIso
|
15 | 4, 14 | eqsstri 3635 |
. 2
|
16 | | funopab4 5925 |
. . 3
OrdIso |
17 | 1 | funeqi 5909 |
. . 3
OrdIso |
18 | 16, 17 | mpbir 221 |
. 2
|
19 | | breq1 4656 |
. . . . . 6
|
20 | 19 | elrab 3363 |
. . . . 5
|
21 | | brdomi 7966 |
. . . . . . 7
|
22 | | f1f 6101 |
. . . . . . . . . . . . . 14
|
23 | 22 | adantl 482 |
. . . . . . . . . . . . 13
|
24 | | frn 6053 |
. . . . . . . . . . . . 13
|
25 | 23, 24 | syl 17 |
. . . . . . . . . . . 12
|
26 | | resss 5422 |
. . . . . . . . . . . . . . 15
|
27 | | ssun2 3777 |
. . . . . . . . . . . . . . 15
|
28 | 26, 27 | sstri 3612 |
. . . . . . . . . . . . . 14
|
29 | | f1oi 6174 |
. . . . . . . . . . . . . . 15
|
30 | | f1of 6137 |
. . . . . . . . . . . . . . 15
|
31 | | fssxp 6060 |
. . . . . . . . . . . . . . 15
|
32 | 29, 30, 31 | mp2b 10 |
. . . . . . . . . . . . . 14
|
33 | 28, 32 | ssini 3836 |
. . . . . . . . . . . . 13
|
34 | 33 | a1i 11 |
. . . . . . . . . . . 12
|
35 | | inss2 3834 |
. . . . . . . . . . . . 13
|
36 | 35 | a1i 11 |
. . . . . . . . . . . 12
|
37 | 25, 34, 36 | 3jca 1242 |
. . . . . . . . . . 11
|
38 | | eloni 5733 |
. . . . . . . . . . . . . . 15
|
39 | | ordwe 5736 |
. . . . . . . . . . . . . . 15
|
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . 14
|
41 | 40 | adantr 481 |
. . . . . . . . . . . . 13
|
42 | | f1f1orn 6148 |
. . . . . . . . . . . . . . . . 17
|
43 | 42 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
44 | | hartogslem.3 |
. . . . . . . . . . . . . . . 16
|
45 | | f1oiso 6601 |
. . . . . . . . . . . . . . . 16
|
46 | 43, 44, 45 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
47 | | isores2 6583 |
. . . . . . . . . . . . . . 15
|
48 | 46, 47 | sylib 208 |
. . . . . . . . . . . . . 14
|
49 | | isowe 6599 |
. . . . . . . . . . . . . 14
|
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
|
51 | 41, 50 | mpbid 222 |
. . . . . . . . . . . 12
|
52 | | weso 5105 |
. . . . . . . . . . . . . . . . . . 19
|
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
54 | | inss2 3834 |
. . . . . . . . . . . . . . . . . . . 20
|
55 | 54 | brel 5168 |
. . . . . . . . . . . . . . . . . . 19
|
56 | 55 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
|
57 | | sonr 5056 |
. . . . . . . . . . . . . . . . . 18
|
58 | 53, 56, 57 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
|
59 | 58 | pm2.01da 458 |
. . . . . . . . . . . . . . . 16
|
60 | 59 | alrimiv 1855 |
. . . . . . . . . . . . . . 15
|
61 | | intirr 5514 |
. . . . . . . . . . . . . . 15
|
62 | 60, 61 | sylibr 224 |
. . . . . . . . . . . . . 14
|
63 | | disj3 4021 |
. . . . . . . . . . . . . 14
|
64 | 62, 63 | sylib 208 |
. . . . . . . . . . . . 13
|
65 | | weeq1 5102 |
. . . . . . . . . . . . 13
|
66 | 64, 65 | syl 17 |
. . . . . . . . . . . 12
|
67 | 51, 66 | mpbid 222 |
. . . . . . . . . . 11
|
68 | 38 | adantr 481 |
. . . . . . . . . . . . 13
|
69 | | isoeq3 6569 |
. . . . . . . . . . . . . . 15
|
70 | 64, 69 | syl 17 |
. . . . . . . . . . . . . 14
|
71 | 48, 70 | mpbid 222 |
. . . . . . . . . . . . 13
|
72 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
73 | 72 | rnex 7100 |
. . . . . . . . . . . . . . 15
|
74 | | exse 5078 |
. . . . . . . . . . . . . . 15
Se |
75 | 73, 74 | ax-mp 5 |
. . . . . . . . . . . . . 14
Se |
76 | | eqid 2622 |
. . . . . . . . . . . . . . 15
OrdIso
OrdIso
|
77 | 76 | oieu 8444 |
. . . . . . . . . . . . . 14
Se
OrdIso
OrdIso |
78 | 67, 75, 77 | sylancl 694 |
. . . . . . . . . . . . 13
OrdIso
OrdIso |
79 | 68, 71, 78 | mpbi2and 956 |
. . . . . . . . . . . 12
OrdIso
OrdIso |
80 | 79 | simpld 475 |
. . . . . . . . . . 11
OrdIso |
81 | 73, 73 | xpex 6962 |
. . . . . . . . . . . . 13
|
82 | 81 | inex2 4800 |
. . . . . . . . . . . 12
|
83 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . . . 20
|
84 | 35, 83 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . 19
|
85 | | dmss 5323 |
. . . . . . . . . . . . . . . . . . 19
|
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
87 | | dmxpid 5345 |
. . . . . . . . . . . . . . . . . 18
|
88 | 86, 87 | syl6sseq 3651 |
. . . . . . . . . . . . . . . . 17
|
89 | | dmresi 5457 |
. . . . . . . . . . . . . . . . . 18
|
90 | | sseq2 3627 |
. . . . . . . . . . . . . . . . . . . 20
|
91 | 33, 90 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . 19
|
92 | | dmss 5323 |
. . . . . . . . . . . . . . . . . . 19
|
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
94 | 89, 93 | syl5eqssr 3650 |
. . . . . . . . . . . . . . . . 17
|
95 | 88, 94 | eqssd 3620 |
. . . . . . . . . . . . . . . 16
|
96 | 95 | sseq1d 3632 |
. . . . . . . . . . . . . . 15
|
97 | 95 | reseq2d 5396 |
. . . . . . . . . . . . . . . 16
|
98 | | id 22 |
. . . . . . . . . . . . . . . 16
|
99 | 97, 98 | sseq12d 3634 |
. . . . . . . . . . . . . . 15
|
100 | 95 | sqxpeqd 5141 |
. . . . . . . . . . . . . . . 16
|
101 | 98, 100 | sseq12d 3634 |
. . . . . . . . . . . . . . 15
|
102 | 96, 99, 101 | 3anbi123d 1399 |
. . . . . . . . . . . . . 14
|
103 | | difeq1 3721 |
. . . . . . . . . . . . . . . . 17
|
104 | | difun2 4048 |
. . . . . . . . . . . . . . . . . . 19
|
105 | 104 | ineq1i 3810 |
. . . . . . . . . . . . . . . . . 18
|
106 | | indif1 3871 |
. . . . . . . . . . . . . . . . . 18
|
107 | | indif1 3871 |
. . . . . . . . . . . . . . . . . 18
|
108 | 105, 106,
107 | 3eqtr3i 2652 |
. . . . . . . . . . . . . . . . 17
|
109 | 103, 108 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
110 | | weeq1 5102 |
. . . . . . . . . . . . . . . 16
|
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . 15
|
112 | | weeq2 5103 |
. . . . . . . . . . . . . . . 16
|
113 | 95, 112 | syl 17 |
. . . . . . . . . . . . . . 15
|
114 | 111, 113 | bitrd 268 |
. . . . . . . . . . . . . 14
|
115 | 102, 114 | anbi12d 747 |
. . . . . . . . . . . . 13
|
116 | | oieq1 8417 |
. . . . . . . . . . . . . . . . 17
OrdIso
OrdIso
|
117 | 109, 116 | syl 17 |
. . . . . . . . . . . . . . . 16
OrdIso
OrdIso
|
118 | | oieq2 8418 |
. . . . . . . . . . . . . . . . 17
OrdIso OrdIso |
119 | 95, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
OrdIso OrdIso |
120 | 117, 119 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
OrdIso
OrdIso
|
121 | 120 | dmeqd 5326 |
. . . . . . . . . . . . . 14
OrdIso
OrdIso
|
122 | 121 | eqeq2d 2632 |
. . . . . . . . . . . . 13
OrdIso
OrdIso |
123 | 115, 122 | anbi12d 747 |
. . . . . . . . . . . 12
OrdIso
OrdIso
|
124 | 82, 123 | spcev 3300 |
. . . . . . . . . . 11
OrdIso
OrdIso |
125 | 37, 67, 80, 124 | syl21anc 1325 |
. . . . . . . . . 10
OrdIso |
126 | 125 | ex 450 |
. . . . . . . . 9
OrdIso |
127 | 126 | exlimdv 1861 |
. . . . . . . 8
OrdIso |
128 | 127 | imp 445 |
. . . . . . 7
OrdIso |
129 | 21, 128 | sylan2 491 |
. . . . . 6
OrdIso |
130 | | simpr 477 |
. . . . . . . . . . 11
OrdIso OrdIso
|
131 | | vex 3203 |
. . . . . . . . . . . . 13
|
132 | 131 | dmex 7099 |
. . . . . . . . . . . 12
|
133 | | eqid 2622 |
. . . . . . . . . . . . 13
OrdIso OrdIso |
134 | 133 | oion 8441 |
. . . . . . . . . . . 12
OrdIso |
135 | 132, 134 | ax-mp 5 |
. . . . . . . . . . 11
OrdIso |
136 | 130, 135 | syl6eqel 2709 |
. . . . . . . . . 10
OrdIso |
137 | 136 | adantl 482 |
. . . . . . . . 9
OrdIso
|
138 | | simplr 792 |
. . . . . . . . . . . . 13
OrdIso
|
139 | 133 | oien 8443 |
. . . . . . . . . . . . 13
OrdIso
|
140 | 132, 138,
139 | sylancr 695 |
. . . . . . . . . . . 12
OrdIso
OrdIso
|
141 | 130, 140 | eqbrtrd 4675 |
. . . . . . . . . . 11
OrdIso |
142 | 141 | adantl 482 |
. . . . . . . . . 10
OrdIso
|
143 | | simpll1 1100 |
. . . . . . . . . . 11
OrdIso
|
144 | | ssdomg 8001 |
. . . . . . . . . . . 12
|
145 | 144 | imp 445 |
. . . . . . . . . . 11
|
146 | 143, 145 | sylan2 491 |
. . . . . . . . . 10
OrdIso
|
147 | | endomtr 8014 |
. . . . . . . . . 10
|
148 | 142, 146,
147 | syl2anc 693 |
. . . . . . . . 9
OrdIso
|
149 | 137, 148 | jca 554 |
. . . . . . . 8
OrdIso
|
150 | 149 | ex 450 |
. . . . . . 7
OrdIso |
151 | 150 | exlimdv 1861 |
. . . . . 6
OrdIso |
152 | 129, 151 | impbid2 216 |
. . . . 5
OrdIso |
153 | 20, 152 | syl5bb 272 |
. . . 4
OrdIso |
154 | 153 | abbi2dv 2742 |
. . 3
OrdIso |
155 | 1 | rneqi 5352 |
. . . 4
OrdIso |
156 | | rnopab 5370 |
. . . 4
OrdIso
OrdIso |
157 | 155, 156 | eqtri 2644 |
. . 3
OrdIso |
158 | 154, 157 | syl6reqr 2675 |
. 2
|
159 | 15, 18, 158 | 3pm3.2i 1239 |
1
|