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

Theorem cvmlift2lem12 27659
Description: Lemma for cvmlift2 27661. (Contributed by Mario Carneiro, 1-Jun-2015.)
Hypotheses
Ref Expression
cvmlift2.b
cvmlift2.f
cvmlift2.g
cvmlift2.p
cvmlift2.i
cvmlift2.h
cvmlift2.k
cvmlift2.m
cvmlift2.a
cvmlift2.s
Assertion
Ref Expression
cvmlift2lem12
Distinct variable groups:   , , , , ,   , , , , , , , ,   , , ,   M, , , , , ,   S, , , , , ,   ,J, , , ,   , , , , , , ,   , , , , ,   , , , , , , , ,   P, , , , ,   , , ,   , , , , , , , ,

Proof of Theorem cvmlift2lem12
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvmlift2.b . . 3
2 cvmlift2.f . . 3
3 cvmlift2.g . . 3
4 cvmlift2.p . . 3
5 cvmlift2.i . . 3
6 cvmlift2.h . . 3
7 cvmlift2.k . . 3
81, 2, 3, 4, 5, 6, 7cvmlift2lem5 27652 . 2
9 iunid 4342 . . . . . . 7
109xpeq2i 4978 . . . . . 6
11 xpiundi 5010 . . . . . 6
1210, 11eqtr3i 2485 . . . . 5
13 cvmlift2.a . . . . . . . 8
14 iiuni 20856 . . . . . . . . 9
15 iicon 20862 . . . . . . . . . 10
1615a1i 11 . . . . . . . . 9
17 inss1 3684 . . . . . . . . . 10
18 iicmp 20861 . . . . . . . . . . . . . . 15
1918a1i 11 . . . . . . . . . . . . . 14
20 iitop 20855 . . . . . . . . . . . . . . 15
2120a1i 11 . . . . . . . . . . . . . 14
2220, 20txtopi 19562 . . . . . . . . . . . . . . . 16
2314neiss2 19104 . . . . . . . . . . . . . . . . . . . . . . . 24
2420, 23mpan 670 . . . . . . . . . . . . . . . . . . . . . . 23
25 vex 3084 . . . . . . . . . . . . . . . . . . . . . . . 24
2625snss 4116 . . . . . . . . . . . . . . . . . . . . . . 23
2724, 26sylibr 212 . . . . . . . . . . . . . . . . . . . . . 22
2827a1d 25 . . . . . . . . . . . . . . . . . . . . 21
2928rexlimiv 2944 . . . . . . . . . . . . . . . . . . . 20
3029adantl 466 . . . . . . . . . . . . . . . . . . 19
31 simpl 457 . . . . . . . . . . . . . . . . . . 19
3230, 31jca 532 . . . . . . . . . . . . . . . . . 18
3332ssopab2i 4733 . . . . . . . . . . . . . . . . 17
34 cvmlift2.s . . . . . . . . . . . . . . . . 17
35 df-xp 4963 . . . . . . . . . . . . . . . . 17
3633, 34, 353sstr4i 3509 . . . . . . . . . . . . . . . 16
3720, 20, 14, 14txunii 19565 . . . . . . . . . . . . . . . . 17
3837ntropn 19052 . . . . . . . . . . . . . . . 16
3922, 36, 38mp2an 672 . . . . . . . . . . . . . . 15
4039a1i 11 . . . . . . . . . . . . . 14
412adantr 465 . . . . . . . . . . . . . . . . . . . 20
423adantr 465 . . . . . . . . . . . . . . . . . . . 20
434adantr 465 . . . . . . . . . . . . . . . . . . . 20
445adantr 465 . . . . . . . . . . . . . . . . . . . 20
45 eqid 2454 . . . . . . . . . . . . . . . . . . . 20
46 simprr 756 . . . . . . . . . . . . . . . . . . . 20
47 simprl 755 . . . . . . . . . . . . . . . . . . . 20
481, 41, 42, 43, 44, 6, 7, 45, 46, 47cvmlift2lem10 27657 . . . . . . . . . . . . . . . . . . 19
4922a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
5036a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
5120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
52 simplrl 759 . . . . . . . . . . . . . . . . . . . . . . . 24
53 simplrr 760 . . . . . . . . . . . . . . . . . . . . . . . 24
54 txopn 19574 . . . . . . . . . . . . . . . . . . . . . . . 24
5551, 51, 52, 53, 54syl22anc 1220 . . . . . . . . . . . . . . . . . . . . . . 23
56 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
57 elunii 4213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5857, 14syl6eleqr 2553 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5956, 53, 58syl2anr 478 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6020a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6152adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
62 simprl 755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
63 opnneip 19122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6460, 61, 62, 63syl3anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6541ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
6642ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
6743ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
6844ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
69 cvmlift2.m . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7053adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
71 simplr2 1031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
72 simprr 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
73 sneq 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7473xpeq2d 4981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7574reseq2d 5227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7674oveq2d 6238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7776oveq1d 6237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7875, 77eleq12d 2536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7978cbvrexv 3057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
80 simplr3 1032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8179, 80syl5bi 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
821, 65, 66, 67, 68, 6, 7, 69, 61, 70, 71, 72, 81cvmlift2lem11 27658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
831, 65, 66, 67, 68, 6, 7, 69, 61, 70, 72, 71, 81cvmlift2lem11 27658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8482, 83impbid 191 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
85 rspe 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8664, 84, 85syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8759, 86jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8887ex 434 . . . . . . . . . . . . . . . . . . . . . . . . 25
8988alrimivv 1687 . . . . . . . . . . . . . . . . . . . . . . . 24
90 df-xp 4963 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9190, 34sseq12i 3496 . . . . . . . . . . . . . . . . . . . . . . . . 25
92 ssopab2b 4732 . . . . . . . . . . . . . . . . . . . . . . . . 25
9391, 92bitri 249 . . . . . . . . . . . . . . . . . . . . . . . 24
9489, 93sylibr 212 . . . . . . . . . . . . . . . . . . . . . . 23
9537ssntr 19061 . . . . . . . . . . . . . . . . . . . . . . 23
9649, 50, 55, 94, 95syl22anc 1220 . . . . . . . . . . . . . . . . . . . . . 22
97 simpr1 994 . . . . . . . . . . . . . . . . . . . . . . 23
98 simpr2 995 . . . . . . . . . . . . . . . . . . . . . . 23
99 opelxpi 4988 . . . . . . . . . . . . . . . . . . . . . . 23
10097, 98, 99syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22