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

Theorem ackbij1lem16 8636
Description: Lemma for ackbij1 8639. (Contributed by Stefan O'Rear, 18-Nov-2014.)
Hypothesis
Ref Expression
ackbij.f
Assertion
Ref Expression
ackbij1lem16
Distinct variable groups:   , ,   , ,   , ,

Proof of Theorem ackbij1lem16
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inss1 3717 . . . . . . . . 9
21sseli 3499 . . . . . . . 8
32elpwid 4022 . . . . . . 7
43adantr 465 . . . . . 6
51sseli 3499 . . . . . . . 8
65elpwid 4022 . . . . . . 7
76adantl 466 . . . . . 6
84, 7unssd 3679 . . . . 5
9 inss2 3718 . . . . . . 7
109sseli 3499 . . . . . 6
119sseli 3499 . . . . . 6
12 unfi 7807 . . . . . 6
1310, 11, 12syl2an 477 . . . . 5
14 nnunifi 7791 . . . . 5
158, 13, 14syl2anc 661 . . . 4
16 peano2 6720 . . . 4
1715, 16syl 16 . . 3
18 ineq2 3693 . . . . . . . 8
1918fveq2d 5875 . . . . . . 7
20 ineq2 3693 . . . . . . . 8
2120fveq2d 5875 . . . . . . 7
2219, 21eqeq12d 2479 . . . . . 6
2318, 20eqeq12d 2479 . . . . . 6
2422, 23imbi12d 320 . . . . 5
2524imbi2d 316 . . . 4
26 ineq2 3693 . . . . . . . 8
2726fveq2d 5875 . . . . . . 7
28 ineq2 3693 . . . . . . . 8
2928fveq2d 5875 . . . . . . 7
3027, 29eqeq12d 2479 . . . . . 6
3126, 28eqeq12d 2479 . . . . . 6
3230, 31imbi12d 320 . . . . 5
3332imbi2d 316 . . . 4
34 ineq2 3693 . . . . . . . 8
3534fveq2d 5875 . . . . . . 7
36 ineq2 3693 . . . . . . . 8
3736fveq2d 5875 . . . . . . 7
3835, 37eqeq12d 2479 . . . . . 6
3934, 36eqeq12d 2479 . . . . . 6
4038, 39imbi12d 320 . . . . 5
4140imbi2d 316 . . . 4
42 ineq2 3693 . . . . . . . 8
4342fveq2d 5875 . . . . . . 7
44 ineq2 3693 . . . . . . . 8
4544fveq2d 5875 . . . . . . 7
4643, 45eqeq12d 2479 . . . . . 6
4742, 44eqeq12d 2479 . . . . . 6
4846, 47imbi12d 320 . . . . 5
4948imbi2d 316 . . . 4
50 in0 3811 . . . . . 6
51 in0 3811 . . . . . 6
5250, 51eqtr4i 2489 . . . . 5
5352a1ii 27 . . . 4
54 simp13 1028 . . . . . . . . . . . . 13
55 3simpa 993 . . . . . . . . . . . . . 14
56 ackbij1lem2 8622 . . . . . . . . . . . . . . . . 17
5756fveq2d 5875 . . . . . . . . . . . . . . . 16
58573ad2ant2 1018 . . . . . . . . . . . . . . 15
59 ackbij1lem4 8624 . . . . . . . . . . . . . . . . . 18
6059adantr 465 . . . . . . . . . . . . . . . . 17
61 simprl 756 . . . . . . . . . . . . . . . . . 18
62 inss1 3717 . . . . . . . . . . . . . . . . . 18
63 ackbij.f . . . . . . . . . . . . . . . . . . 19
6463ackbij1lem11 8631 . . . . . . . . . . . . . . . . . 18
6561, 62, 64sylancl 662 . . . . . . . . . . . . . . . . 17
66 incom 3690 . . . . . . . . . . . . . . . . . 18
67 inss2 3718 . . . . . . . . . . . . . . . . . . 19
68 nnord 6708 . . . . . . . . . . . . . . . . . . . . 21
69 orddisj 4921 . . . . . . . . . . . . . . . . . . . . 21
7068, 69syl 16 . . . . . . . . . . . . . . . . . . . 20
7170adantr 465 . . . . . . . . . . . . . . . . . . 19
72 ssdisj 3876 . . . . . . . . . . . . . . . . . . 19
7367, 71, 72sylancr 663 . . . . . . . . . . . . . . . . . 18
7466, 73syl5eq 2510 . . . . . . . . . . . . . . . . 17
7563ackbij1lem9 8629 . . . . . . . . . . . . . . . . 17
7660, 65, 74, 75syl3anc 1228 . . . . . . . . . . . . . . . 16
77763ad2ant1 1017 . . . . . . . . . . . . . . 15
7858, 77eqtrd 2498 . . . . . . . . . . . . . 14
7955, 78syl3an1 1261 . . . . . . . . . . . . 13
80 ackbij1lem2 8622 . . . . . . . . . . . . . . . . 17
8180fveq2d 5875 . . . . . . . . . . . . . . . 16
82813ad2ant3 1019 . . . . . . . . . . . . . . 15
83 simprr 757 . . . . . . . . . . . . . . . . . 18
84 inss1 3717 . . . . . . . . . . . . . . . . . 18
8563ackbij1lem11 8631 . . . . . . . . . . . . . . . . . 18
8683, 84, 85sylancl 662 . . . . . . . . . . . . . . . . 17
87 incom 3690 . . . . . . . . . . . . . . . . . 18
88 inss2 3718 . . . . . . . . . . . . . . . . . . 19
89 ssdisj 3876 . . . . . . . . . . . . . . . . . . 19
9088, 71, 89sylancr 663 . . . . . . . . . . . . . . . . . 18
9187, 90syl5eq 2510 . . . . . . . . . . . . . . . . 17
9263ackbij1lem9 8629 . . . . . . . . . . . . . . . . 17
9360, 86, 91, 92syl3anc 1228 . . . . . . . . . . . . . . . 16
94933ad2ant1 1017 . . . . . . . . . . . . . . 15
9582, 94eqtrd 2498 . . . . . . . . . . . . . 14
9655, 95syl3an1 1261 . . . . . . . . . . . . 13
9754, 79, 963eqtr3d 2506 . . . . . . . . . . . 12
9863ackbij1lem10 8630 . . . . . . . . . . . . . . . . 17
9998ffvelrni 6030 . . . . . . . . . . . . . . . 16
10060, 99syl 16 . . . . . . . . . . . . . . 15
10198ffvelrni 6030 . . . . . . . . . . . . . . . 16
10265, 101syl 16 . . . . . . . . . . . . . . 15
10398ffvelrni 6030 . . . . . . . . . . . . . . . 16
10486, 103syl 16 . . . . . . . . . . . . . . 15
105 nnacan 7296 . . . . . . . . . . . . . . 15
106100, 102, 104, 105syl3anc 1228 . . . . . . . . . . . . . 14
1071063adant3 1016 . . . . . . . . . . . . 13
1081073ad2ant1 1017 . . . . . . . . . . . 12
10997, 108mpbid 210 . . . . . . . . . . 11
110 uneq2 3651 . . . . . . . . . . . . . . 15
111110adantl 466 . . . . . . . . . . . . . 14
11256ad2antrr 725 . . . . . . . . . . . . . 14
11380ad2antlr 726 . . . . . . . . . . . . . 14
114111, 112, 1133eqtr4d 2508 . . . . . . . . . . . . 13
115114ex 434 . . . . . . . . . . . 12
1161153adant1 1014 . . . . . . . . . . 11
117109, 116embantd 54 . . . . . . . . . 10
1181173exp 1195 . . . . . . . . 9
119 simp13 1028 . . . . . . . . . . . 12
120119eqcomd 2465 . . . . . . . . . . 11
121 simp12r 1110 . . . . . . . . . . . 12
122 simp12l 1109 . . . . . . . . . . . 12
123 simp11 1026 . . . . . . . . . . . 12
124 simp3 998 . . . . . . . . . . . 12
125 simp2 997 . . . . . . . . . . . 12
12663ackbij1lem15 8635 . . . . . . . . . . . 12
127121, 122, 123, 124, 125, 126syl23anc 1235 . . . . . . . . . . 11
128120, 127pm2.21dd 174 . . . . . . . . . 10
1291283exp 1195 . . . . . . . . 9
130118, 129pm2.61d 158 . . . . . . . 8
131 simp13 1028 . . . . . . . . . . 11
132 simp12l 1109 . . . . . . . . . . . 12
133 simp12r 1110 . . . . . . . . . . . 12
134 simp11 1026 . . . . . . . . . . . 12
135 simp2 997 . . . . . . . . . . . 12
136 simp3 998 . . . . . . . . . . . 12
13763ackbij1lem15 8635 . . . . . . . . . . . 12
138132, 133, 134, 135, 136, 137syl23anc 1235 . . . . . . . . . . 11
139131, 138pm2.21dd 174 . . . . . . . . . 10
1401393exp 1195 . . . . . . . . 9
141 simp13 1028 . . . . . . . . . . . 12
142 ackbij1lem1 8621 . . . . . . . . . . . . . . . . 17
143142adantr 465 . . . . . . . . . . . . . . . 16