Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmlift3lem2 Unicode version

Theorem cvmlift3lem2 26912
Description: Lemma for cvmlift2 26908. (Contributed by Mario Carneiro, 6-Jul-2015.)
Hypotheses
Ref Expression
cvmlift3.b
cvmlift3.y
cvmlift3.f
cvmlift3.k
cvmlift3.l
cvmlift3.o
cvmlift3.g
cvmlift3.p
cvmlift3.e
Assertion
Ref Expression
cvmlift3lem2
Distinct variable groups:   , ,   ,J,   , , ,   , , ,   , , ,   , , ,   , , ,   ,   , , ,   P, , ,   ,O, ,   , , ,

Proof of Theorem cvmlift3lem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvmlift3.k . . . . 5
21adantr 455 . . . 4
3 sconpcon 26819 . . . 4
42, 3syl 16 . . 3
5 cvmlift3.o . . . 4
65adantr 455 . . 3
7 simpr 451 . . 3
8 cvmlift3.y . . . 4
98pconcn 26816 . . 3
104, 6, 7, 9syl3anc 1203 . 2
11 cvmlift3.b . . . . . . . . 9
12 eqid 2422 . . . . . . . . 9
13 cvmlift3.f . . . . . . . . . 10
1413ad2antrr 710 . . . . . . . . 9
15 simprl 740 . . . . . . . . . 10
16 cvmlift3.g . . . . . . . . . . 11
1716ad2antrr 710 . . . . . . . . . 10
18 cnco 18574 . . . . . . . . . 10
1915, 17, 18syl2anc 646 . . . . . . . . 9
20 cvmlift3.p . . . . . . . . . 10
2120ad2antrr 710 . . . . . . . . 9
22 simprrl 748 . . . . . . . . . . 11
2322fveq2d 5665 . . . . . . . . . 10
24 iiuni 20157 . . . . . . . . . . . . 13
2524, 8cnf 18554 . . . . . . . . . . . 12
2615, 25syl 16 . . . . . . . . . . 11
27 0elunit 11347 . . . . . . . . . . 11
28 fvco3 5738 . . . . . . . . . . 11
2926, 27, 28sylancl 647 . . . . . . . . . 10
30 cvmlift3.e . . . . . . . . . . 11
3130ad2antrr 710 . . . . . . . . . 10
3223, 29, 313eqtr4rd 2465 . . . . . . . . 9
3311, 12, 14, 19, 21, 32cvmliftiota 26893 . . . . . . . 8
3433simp1d 985 . . . . . . 7
3524, 11cnf 18554 . . . . . . 7
3634, 35syl 16 . . . . . 6
37 1elunit 11348 . . . . . 6
38 ffvelrn 5811 . . . . . 6
3936, 37, 38sylancl 647 . . . . 5
40 simprrr 749 . . . . . 6
41 eqidd 2423 . . . . . 6
42 fveq1 5660 . . . . . . . . 9
4342eqeq1d 2430 . . . . . . . 8
44 fveq1 5660 . . . . . . . . 9
4544eqeq1d 2430 . . . . . . . 8
46 coeq2 4969 . . . . . . . . . . . . 13
4746eqeq2d 2433 . . . . . . . . . . . 12
4847anbi1d 689 . . . . . . . . . . 11
4948riotabidv 6022 . . . . . . . . . 10
5049fveq1d 5663 . . . . . . . . 9
5150eqeq1d 2430 . . . . . . . 8
5243, 45, 513anbi123d 1274 . . . . . . 7
5352rspcev 3051 . . . . . 6
5415, 22, 40, 41, 53syl13anc 1205 . . . . 5
5513ad4antr 716 . . . . . . . . 9
561ad4antr 716 . . . . . . . . 9
57 cvmlift3.l . . . . . . . . . 10
5857ad4antr 716 . . . . . . . . 9
595ad4antr 716 . . . . . . . . 9
6016ad4antr 716 . . . . . . . . 9
6120ad4antr 716 . . . . . . . . 9
6230ad4antr 716 . . . . . . . . 9
6315ad2antrr 710 . . . . . . . . 9
6422ad2antrr 710 . . . . . . . . 9
65 simprl 740 . . . . . . . . 9
66 simprr1 1021 . . . . . . . . 9
6740ad2antrr 710 . . . . . . . . . 10
68 simprr2 1022 . . . . . . . . . 10
6967, 68eqtr4d 2457 . . . . . . . . 9
7011, 8, 55, 56, 58, 59, 60, 61, 62, 63, 64, 65, 66, 69cvmlift3lem1 26911 . . . . . . . 8
71 simprr3 1023 . . . . . . . 8
7270, 71eqtrd 2454 . . . . . . 7
7372rexlimdvaa 2821 . . . . . 6
7473ralrimiva 2778 . . . . 5
75 eqeq2 2431 . . . . . . . . 9
76753anbi3d 1280 . . . . . . . 8
7776rexbidv 2715 . . . . . . 7
78 eqeq1 2428 . . . . . . . . 9
7978imbi2d 310 . . . . . . . 8
8079ralbidv 2714 . . . . . . 7
8177, 80anbi12d 695 . . . . . 6
8281rspcev 3051 . . . . 5
8339, 54, 74, 82syl12anc 1201 . . . 4
84 fveq1 5660 . . . . . . . . 9
8584eqeq1d 2430 . . . . . . . 8
86 fveq1 5660 . . . . . . . . 9
8786eqeq1d 2430 . . . . . . . 8
88 coeq2 4969 . . . . . . . . . . . . 13
8988eqeq2d 2433 . . . . . . . . . . . 12
9089anbi1d 689 . . . . . . . . . . 11
9190riotabidv 6022 . . . . . . . . . 10
9291fveq1d 5663 . . . . . . . . 9
9392eqeq1d 2430 . . . . . . . 8
9485, 87, 933anbi123d 1274 . . . . . . 7
9594cbvrexv 2927 . . . . . 6
96 eqeq2 2431 . . . . . . . 8
97963anbi3d 1280 . . . . . . 7
9897rexbidv 2715 . . . . . 6