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

Theorem mreexexlem4d 14921
 Description: Induction step of the induction in mreexexd 14922. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
mreexexlem2d.1 Moore
mreexexlem2d.2 mrCls
mreexexlem2d.3 mrInd
mreexexlem2d.4
mreexexlem2d.5
mreexexlem2d.6
mreexexlem2d.7
mreexexlem2d.8
mreexexlem4d.9
mreexexlem4d.A
mreexexlem4d.B
Assertion
Ref Expression
mreexexlem4d
Distinct variable groups:   ,,,   ,,,,   ,,,   ,,,   ,,,   ,,,   ,,,   ,,,   ,,,   ,   ,   ,   ,,
Allowed substitution hints:   (,,,)   (,,,,,,)   (,,)   (,,)   (,,)   (,,)   (,,,)   ()   (,)

Proof of Theorem mreexexlem4d
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mreexexlem2d.1 . . . 4 Moore
21adantr 465 . . 3 Moore
3 mreexexlem2d.2 . . 3 mrCls
4 mreexexlem2d.3 . . 3 mrInd
5 mreexexlem2d.4 . . . 4
7 mreexexlem2d.5 . . . 4
9 mreexexlem2d.6 . . . 4
11 mreexexlem2d.7 . . . 4
13 mreexexlem2d.8 . . . 4
15 simpr 461 . . . 4
1615orcd 392 . . 3
172, 3, 4, 6, 8, 10, 12, 14, 16mreexexlem3d 14920 . 2
18 n0 3780 . . . . 5
1918biimpi 194 . . . 4
211adantr 465 . . . . . 6 Moore
225adantr 465 . . . . . 6
237adantr 465 . . . . . 6
249adantr 465 . . . . . 6
2511adantr 465 . . . . . 6
2613adantr 465 . . . . . 6
27 simpr 461 . . . . . 6
2821, 3, 4, 22, 23, 24, 25, 26, 27mreexexlem2d 14919 . . . . 5
29 3anass 978 . . . . . 6
301ad2antrr 725 . . . . . . . . 9 Moore
3130elfvexd 5884 . . . . . . . 8
32 simpr2 1004 . . . . . . . . . . 11
33 difsnb 4157 . . . . . . . . . . 11
3432, 33sylib 196 . . . . . . . . . 10
357ad2antrr 725 . . . . . . . . . . . 12
3635ssdifssd 3627 . . . . . . . . . . 11
3736ssdifd 3625 . . . . . . . . . 10
3834, 37eqsstr3d 3524 . . . . . . . . 9
39 difun1 3743 . . . . . . . . 9
4038, 39syl6sseqr 3536 . . . . . . . 8
419ad2antrr 725 . . . . . . . . . 10
4241ssdifd 3625 . . . . . . . . 9
4342, 39syl6sseqr 3536 . . . . . . . 8
4411ad2antrr 725 . . . . . . . . . 10
45 simpr1 1003 . . . . . . . . . . . 12
46 uncom 3633 . . . . . . . . . . . . . 14
4746uneq2i 3640 . . . . . . . . . . . . 13
48 unass 3646 . . . . . . . . . . . . . 14
49 difsnid 4161 . . . . . . . . . . . . . . 15
5049uneq1d 3642 . . . . . . . . . . . . . 14
5148, 50syl5eqr 2498 . . . . . . . . . . . . 13
5247, 51syl5eq 2496 . . . . . . . . . . . 12
5345, 52syl 16 . . . . . . . . . . 11
5453fveq2d 5860 . . . . . . . . . 10
5544, 54sseqtr4d 3526 . . . . . . . . 9
5655ssdifssd 3627 . . . . . . . 8
57 simpr3 1005 . . . . . . . 8
58 mreexexlem4d.B . . . . . . . . . 10
5958ad2antrr 725 . . . . . . . . 9
60 mreexexlem4d.9 . . . . . . . . . . . 12
6160ad2antrr 725 . . . . . . . . . . 11
62 simplr 755 . . . . . . . . . . 11
63 3anan12 987 . . . . . . . . . . . . 13
64 dif1en 7755 . . . . . . . . . . . . 13
6563, 64sylbir 213 . . . . . . . . . . . 12
6665expcom 435 . . . . . . . . . . 11
6761, 62, 66syl2anc 661 . . . . . . . . . 10
68 3anan12 987 . . . . . . . . . . . . 13
69 dif1en 7755 . . . . . . . . . . . . 13
7068, 69sylbir 213 . . . . . . . . . . . 12
7170expcom 435 . . . . . . . . . . 11
7261, 45, 71syl2anc 661 . . . . . . . . . 10
7367, 72orim12d 838 . . . . . . . . 9
7459, 73mpd 15 . . . . . . . 8
75 mreexexlem4d.A . . . . . . . . 9
7675ad2antrr 725 . . . . . . . 8
7731, 40, 43, 56, 57, 74, 76mreexexlemd 14918 . . . . . . 7
78 simprl 756 . . . . . . . . . . . 12
7978elpwid 4007 . . . . . . . . . . 11
8079difss2d 3619 . . . . . . . . . 10
81 simplr1 1039 . . . . . . . . . . 11
8281snssd 4160 . . . . . . . . . 10
8380, 82unssd 3665 . . . . . . . . 9
8431adantr 465 . . . . . . . . . . 11
859ad3antrrr 729 . . . . . . . . . . . 12
8685difss2d 3619 . . . . . . . . . . 11
8784, 86ssexd 4584 . . . . . . . . . 10
88 elpw2g 4600 . . . . . . . . . 10
8987, 88syl 16 . . . . . . . . 9
9083, 89mpbird 232 . . . . . . . 8
91 difsnid 4161 . . . . . . . . . 10
9291ad3antlr 730 . . . . . . . . 9
93 simprrl 765 . . . . . . . . . 10
94 vex 3098 . . . . . . . . . . . 12
95 vex 3098 . . . . . . . . . . . 12
96 en2sn 7597 . . . . . . . . . . . 12
9794, 95, 96mp2an 672 . . . . . . . . . . 11
9897a1i 11 . . . . . . . . . 10
99 incom 3676 . . . . . . . . . . . 12
100 disjdif 3886 . . . . . . . . . . . 12
10199, 100eqtri 2472 . . . . . . . . . . 11
102101a1i 11 . . . . . . . . . 10
103 ssdifin0 3895 . . . . . . . . . . 11
10479, 103syl 16 . . . . . . . . . 10
105 unen 7600 . . . . . . . . . 10
10693, 98, 102, 104, 105syl22anc 1230 . . . . . . . . 9
10792, 106eqbrtrrd 4459 . . . . . . . 8
108 unass 3646 . . . . . . . . . 10
109 uncom 3633 . . . . . . . . . . 11
110109uneq2i 3640 . . . . . . . . . 10
111108, 110eqtr2i 2473 . . . . . . . . 9
112 simprrr 766 . . . . . . . . 9
113111, 112syl5eqelr 2536 . . . . . . . 8
114 breq2 4441 . . . . . . . . . 10
115 uneq1 3636 . . . . . . . . . . 11
116115eleq1d 2512 . . . . . . . . . 10
117114, 116anbi12d 710 . . . . . . . . 9
118117rspcev 3196 . . . . . . . 8
11990, 107, 113, 118syl12anc 1227 . . . . . . 7
12077, 119rexlimddv 2939 . . . . . 6
12129, 120sylan2br 476 . . . . 5
12228, 121rexlimddv 2939 . . . 4