MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hartogslem1 Unicode version

Theorem hartogslem1 7988
Description: Lemma for hartogs 7990. (Contributed by Mario Carneiro, 14-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.)
Hypotheses
Ref Expression
hartogslem.2
hartogslem.3
Assertion
Ref Expression
hartogslem1
Distinct variable groups:   , , , , ,   , , , ,   , ,   , ,

Proof of Theorem hartogslem1
StepHypRef Expression
1 hartogslem.2 . . . . 5
21dmeqi 5209 . . . 4
3 dmopab 5218 . . . 4
42, 3eqtri 2486 . . 3
5 simp3 998 . . . . . . . 8
6 simp1 996 . . . . . . . . 9
7 xpss12 5113 . . . . . . . . 9
86, 6, 7syl2anc 661 . . . . . . . 8
95, 8sstrd 3513 . . . . . . 7
10 selpw 4019 . . . . . . 7
119, 10sylibr 212 . . . . . 6
1211ad2antrr 725 . . . . 5
1312exlimiv 1722 . . . 4
1413abssi 3574 . . 3
154, 14eqsstri 3533 . 2
16 funopab4 5628 . . 3
171funeqi 5613 . . 3
1816, 17mpbir 209 . 2
19 breq1 4455 . . . . . 6
2019elrab 3257 . . . . 5
21 brdomi 7547 . . . . . . 7
22 f1f 5786 . . . . . . . . . . . . . 14
2322adantl 466 . . . . . . . . . . . . 13
24 frn 5742 . . . . . . . . . . . . 13
2523, 24syl 16 . . . . . . . . . . . 12
26 resss 5302 . . . . . . . . . . . . . . 15
27 ssun2 3667 . . . . . . . . . . . . . . 15
2826, 27sstri 3512 . . . . . . . . . . . . . 14
29 f1oi 5856 . . . . . . . . . . . . . . 15
30 f1of 5821 . . . . . . . . . . . . . . 15
31 fssxp 5748 . . . . . . . . . . . . . . 15
3229, 30, 31mp2b 10 . . . . . . . . . . . . . 14
3328, 32ssini 3720 . . . . . . . . . . . . 13
3433a1i 11 . . . . . . . . . . . 12
35 inss2 3718 . . . . . . . . . . . . 13
3635a1i 11 . . . . . . . . . . . 12
3725, 34, 363jca 1176 . . . . . . . . . . 11
38 eloni 4893 . . . . . . . . . . . . . . 15
39 ordwe 4896 . . . . . . . . . . . . . . 15
4038, 39syl 16 . . . . . . . . . . . . . 14
4140adantr 465 . . . . . . . . . . . . 13
42 f1f1orn 5832 . . . . . . . . . . . . . . . . 17
4342adantl 466 . . . . . . . . . . . . . . . 16
44 hartogslem.3 . . . . . . . . . . . . . . . 16
45 f1oiso 6247 . . . . . . . . . . . . . . . 16
4643, 44, 45sylancl 662 . . . . . . . . . . . . . . 15
47 isores2 6229 . . . . . . . . . . . . . . 15
4846, 47sylib 196 . . . . . . . . . . . . . 14
49 isowe 6245 . . . . . . . . . . . . . 14
5048, 49syl 16 . . . . . . . . . . . . 13
5141, 50mpbid 210 . . . . . . . . . . . 12
52 weso 4875 . . . . . . . . . . . . . . . . . . 19
5351, 52syl 16 . . . . . . . . . . . . . . . . . 18
54 inss2 3718 . . . . . . . . . . . . . . . . . . . 20
5554brel 5053 . . . . . . . . . . . . . . . . . . 19
5655simpld 459 . . . . . . . . . . . . . . . . . 18
57 sonr 4826 . . . . . . . . . . . . . . . . . 18
5853, 56, 57syl2an 477 . . . . . . . . . . . . . . . . 17
5958pm2.01da 442 . . . . . . . . . . . . . . . 16
6059alrimiv 1719 . . . . . . . . . . . . . . 15
61 intirr 5390 . . . . . . . . . . . . . . 15
6260, 61sylibr 212 . . . . . . . . . . . . . 14
63 disj3 3871 . . . . . . . . . . . . . 14
6462, 63sylib 196 . . . . . . . . . . . . 13
65 weeq1 4872 . . . . . . . . . . . . 13
6664, 65syl 16 . . . . . . . . . . . 12
6751, 66mpbid 210 . . . . . . . . . . 11
6838adantr 465 . . . . . . . . . . . . 13
69 isoeq3 6217 . . . . . . . . . . . . . . 15
7064, 69syl 16 . . . . . . . . . . . . . 14
7148, 70mpbid 210 . . . . . . . . . . . . 13
72 vex 3112 . . . . . . . . . . . . . . . 16
7372rnex 6734 . . . . . . . . . . . . . . 15
74 exse 4848 . . . . . . . . . . . . . . 15
7573, 74ax-mp 5 . . . . . . . . . . . . . 14
76 eqid 2457 . . . . . . . . . . . . . . 15
7776oieu 7985 . . . . . . . . . . . . . 14
7867, 75, 77sylancl 662 . . . . . . . . . . . . 13
7968, 71, 78mpbi2and 921 . . . . . . . . . . . 12
8079simpld 459 . . . . . . . . . . 11
8173, 73xpex 6604 . . . . . . . . . . . . 13
8281inex2 4594 . . . . . . . . . . . 12
83 sseq1 3524 . . . . . . . . . . . . . . . . . . . 20
8435, 83mpbiri 233 . . . . . . . . . . . . . . . . . . 19
85 dmss 5207 . . . . . . . . . . . . . . . . . . 19
8684, 85syl 16 . . . . . . . . . . . . . . . . . 18
87 dmxpid 5227 . . . . . . . . . . . . . . . . . 18
8886, 87syl6sseq 3549 . . . . . . . . . . . . . . . . 17
89 dmresi 5334 . . . . . . . . . . . . . . . . . 18
90 sseq2 3525 . . . . . . . . . . . . . . . . . . . 20
9133, 90mpbiri 233 . . . . . . . . . . . . . . . . . . 19
92 dmss 5207 . . . . . . . . . . . . . . . . . . 19
9391, 92syl 16 . . . . . . . . . . . . . . . . . 18
9489, 93syl5eqssr 3548 . . . . . . . . . . . . . . . . 17
9588, 94eqssd 3520 . . . . . . . . . . . . . . . 16
9695sseq1d 3530 . . . . . . . . . . . . . . 15
9795reseq2d 5278 . . . . . . . . . . . . . . . 16
98 id 22 . . . . . . . . . . . . . . . 16
9997, 98sseq12d 3532 . . . . . . . . . . . . . . 15
10095sqxpeqd 5030 . . . . . . . . . . . . . . . 16
10198, 100sseq12d 3532 . . . . . . . . . . . . . . 15
10296, 99, 1013anbi123d 1299 . . . . . . . . . . . . . 14
103 difeq1 3614 . . . . . . . . . . . . . . . . 17
104 difun2 3907 . . . . . . . . . . . . . . . . . . 19
105104ineq1i 3695 . . . . . . . . . . . . . . . . . 18
106 indif1 3741 . . . . . . . . . . . . . . . . . 18
107 indif1 3741 . . . . . . . . . . . . . . . . . 18
108105, 106, 1073eqtr3i 2494 . . . . . . . . . . . . . . . . 17
109103, 108syl6eq 2514 . . . . . . . . . . . . . . . 16
110 weeq1 4872 . . . . . . . . . . . . . . . 16
111109, 110syl 16 . . . . . . . . . . . . . . 15
112 weeq2 4873 . . . . . . . . . . . . . . . 16
11395, 112syl 16 . . . . . . . . . . . . . . 15
114111, 113bitrd 253 . . . . . . . . . . . . . 14
115102, 114anbi12d 710 . . . . . . . . . . . . 13
116 oieq1 7958 . . . . . . . . . . . . . . . . 17
117109, 116syl 16 . . . . . . . . . . . . . . . 16
118 oieq2 7959 . . . . . . . . . . . . . . . . 17
11995, 118syl 16 . . . . . . . . . . . . . . . 16
120117, 119eqtrd 2498 . . . . . . . . . . . . . . 15
121120dmeqd 5210 . . . . . . . . . . . . . 14
122121eqeq2d 2471 . . . . . . . . . . . . 13
123115, 122anbi12d 710 . . . . . . . . . . . 12
12482, 123spcev 3201 . . . . . . . . . . 11
12537, 67, 80, 124syl21anc 1227 . . . . . . . . . 10
126125ex 434 . . . . . . . . 9
127126exlimdv 1724 . . . . . . . 8
128127imp 429 . . . . . . 7
12921, 128sylan2 474 . . . . . 6
130 simpr 461 . . . . . . . . . . 11
131 vex 3112 . . . . . . . . . . . . 13
132131dmex 6733 . . . . . . . . . . . 12
133 eqid 2457 . . . . . . . . . . . . 13
134133oion 7982 . . . . . . . . . . . 12
135132, 134ax-mp 5 . . . . . . . . . . 11
136130, 135syl6eqel 2553 . . . . . . . . . 10
137136adantl 466 . . . . . . . . 9
138 simplr 755 . . . . . . . . . . . . 13
139133oien 7984 . . . . . . . . . . . . 13
140132, 138, 139sylancr 663 . . . . . . . . . . . 12