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

Theorem cvmlift2lem12 26906
Description: Lemma for cvmlift2 26908. (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 26899 . 2
9 iunid 4200 . . . . . . 7
109xpeq2i 4832 . . . . . 6
11 xpiundi 4864 . . . . . 6
1210, 11eqtr3i 2444 . . . . 5
13 cvmlift2.a . . . . . . . 8
14 iiuni 20157 . . . . . . . . 9
15 iicon 20163 . . . . . . . . . 10
1615a1i 11 . . . . . . . . 9
17 inss1 3547 . . . . . . . . . 10
18 iicmp 20162 . . . . . . . . . . . . . . 15
1918a1i 11 . . . . . . . . . . . . . 14
20 iitop 20156 . . . . . . . . . . . . . . 15
2120a1i 11 . . . . . . . . . . . . . 14
2220, 20txtopi 18867 . . . . . . . . . . . . . . . 16
2314neiss2 18409 . . . . . . . . . . . . . . . . . . . . . . . 24
2420, 23mpan 655 . . . . . . . . . . . . . . . . . . . . . . 23
25 vex 2954 . . . . . . . . . . . . . . . . . . . . . . . 24
2625snss 3974 . . . . . . . . . . . . . . . . . . . . . . 23
2724, 26sylibr 206 . . . . . . . . . . . . . . . . . . . . . 22
2827a1d 24 . . . . . . . . . . . . . . . . . . . . 21
2928rexlimiv 2814 . . . . . . . . . . . . . . . . . . . 20
3029adantl 456 . . . . . . . . . . . . . . . . . . 19
31 simpl 447 . . . . . . . . . . . . . . . . . . 19
3230, 31jca 522 . . . . . . . . . . . . . . . . . 18
3332ssopab2i 4589 . . . . . . . . . . . . . . . . 17
34 cvmlift2.s . . . . . . . . . . . . . . . . 17
35 df-xp 4817 . . . . . . . . . . . . . . . . 17
3633, 34, 353sstr4i 3372 . . . . . . . . . . . . . . . 16
3720, 20, 14, 14txunii 18870 . . . . . . . . . . . . . . . . 17
3837ntropn 18357 . . . . . . . . . . . . . . . 16
3922, 36, 38mp2an 657 . . . . . . . . . . . . . . 15
4039a1i 11 . . . . . . . . . . . . . 14
412adantr 455 . . . . . . . . . . . . . . . . . . . 20
423adantr 455 . . . . . . . . . . . . . . . . . . . 20
434adantr 455 . . . . . . . . . . . . . . . . . . . 20
445adantr 455 . . . . . . . . . . . . . . . . . . . 20
45 eqid 2422 . . . . . . . . . . . . . . . . . . . 20
46 simprr 741 . . . . . . . . . . . . . . . . . . . 20
47 simprl 740 . . . . . . . . . . . . . . . . . . . 20
481, 41, 42, 43, 44, 6, 7, 45, 46, 47cvmlift2lem10 26904 . . . . . . . . . . . . . . . . . . 19
4922a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
5036a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
5120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
52 simplrl 744 . . . . . . . . . . . . . . . . . . . . . . . 24
53 simplrr 745 . . . . . . . . . . . . . . . . . . . . . . . 24
54 txopn 18879 . . . . . . . . . . . . . . . . . . . . . . . 24
5551, 51, 52, 53, 54syl22anc 1204 . . . . . . . . . . . . . . . . . . . . . . 23
56 simpr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
57 elunii 4071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5857, 14syl6eleqr 2513 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5956, 53, 58syl2anr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6020a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6152adantr 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
62 simprl 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
63 opnneip 18427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6460, 61, 62, 63syl3anc 1203 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6541ad3antrrr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
6642ad3antrrr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
6743ad3antrrr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
6844ad3antrrr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
69 cvmlift2.m . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7053adantr 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
71 simplr2 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
72 simprr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
73 sneq 3864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7473xpeq2d 4835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7574reseq2d 5081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7674oveq2d 6077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7776oveq1d 6076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7875, 77eleq12d 2490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7978cbvrexv 2927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
80 simplr3 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8179, 80syl5bi 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
821, 65, 66, 67, 68, 6, 7, 69, 61, 70, 71, 72, 81cvmlift2lem11 26905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
831, 65, 66, 67, 68, 6, 7, 69, 61, 70, 72, 71, 81cvmlift2lem11 26905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8482, 83impbid 185 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
85 rspe 2756 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8664, 84, 85syl2anc 646 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8759, 86jca 522 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8887ex 427 . . . . . . . . . . . . . . . . . . . . . . . . 25
8988alrimivv 1677 . . . . . . . . . . . . . . . . . . . . . . . 24
90 df-xp 4817 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9190, 34sseq12i 3359 . . . . . . . . . . . . . . . . . . . . . . . . 25
92 ssopab2b 4588 . . . . . . . . . . . . . . . . . . . . . . . . 25
9391, 92bitri 243 . . . . . . . . . . . . . . . . . . . . . . . 24
9489, 93sylibr 206 . . . . . . . . . . . . . . . . . . . . . . 23
9537ssntr 18366 . . . . . . . . . . . . . . . . . . . . . . 23
9649, 50, 55, 94, 95syl22anc 1204 . . . . . . . . . . . . . . . . . . . . . 22
97 simpr1 979 . . . . . . . . . . . . . . . . . . . . . . 23
98 simpr2 980 . . . . . . . . . . . . . . . . . . . . . . 23
99 opelxpi 4842 . . . . . . . . . . . . . . . . . . . . . . 23
10097, 98, 99syl2anc 646 . . . . . . . . . . . . . . . . . . . . . 22