Step | Hyp | Ref
| Expression |
1 | | cvmlift2.f |
. . 3
CovMap |
2 | | cvmlift2.g |
. . . . 5
|
3 | | iitop 22683 |
. . . . . . 7
|
4 | | iiuni 22684 |
. . . . . . 7
|
5 | 3, 3, 4, 4 | txunii 21396 |
. . . . . 6
|
6 | | eqid 2622 |
. . . . . 6
|
7 | 5, 6 | cnf 21050 |
. . . . 5
|
8 | 2, 7 | syl 17 |
. . . 4
|
9 | | cvmlift2lem10.1 |
. . . . 5
|
10 | | cvmlift2lem10.2 |
. . . . 5
|
11 | 9, 10 | opelxpd 5149 |
. . . 4
|
12 | 8, 11 | ffvelrnd 6360 |
. . 3
|
13 | | cvmlift2lem10.s |
. . . 4
↾t
↾t |
14 | 13, 6 | cvmcov 31245 |
. . 3
CovMap
|
15 | 1, 12, 14 | syl2anc 693 |
. 2
|
16 | | n0 3931 |
. . . . 5
|
17 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
18 | | opelxp 5146 |
. . . . . . . . . . . . 13
|
19 | 17, 18 | syl6bb 276 |
. . . . . . . . . . . 12
|
20 | 19 | anbi1d 741 |
. . . . . . . . . . 11
|
21 | 20 | 2rexbidv 3057 |
. . . . . . . . . 10
|
22 | 2 | adantr 481 |
. . . . . . . . . . . 12
|
23 | 13 | cvmsrcl 31246 |
. . . . . . . . . . . . 13
|
24 | 23 | ad2antll 765 |
. . . . . . . . . . . 12
|
25 | | cnima 21069 |
. . . . . . . . . . . 12
|
26 | 22, 24, 25 | syl2anc 693 |
. . . . . . . . . . 11
|
27 | | eltx 21371 |
. . . . . . . . . . . 12
|
28 | 3, 3, 27 | mp2an 708 |
. . . . . . . . . . 11
|
29 | 26, 28 | sylib 208 |
. . . . . . . . . 10
|
30 | 11 | adantr 481 |
. . . . . . . . . . 11
|
31 | | simprl 794 |
. . . . . . . . . . 11
|
32 | 8 | adantr 481 |
. . . . . . . . . . . 12
|
33 | | ffn 6045 |
. . . . . . . . . . . 12
|
34 | | elpreima 6337 |
. . . . . . . . . . . 12
|
35 | 32, 33, 34 | 3syl 18 |
. . . . . . . . . . 11
|
36 | 30, 31, 35 | mpbir2and 957 |
. . . . . . . . . 10
|
37 | 21, 29, 36 | rspcdva 3316 |
. . . . . . . . 9
|
38 | | iillysconn 31235 |
. . . . . . . . . . . . 13
Locally SConn |
39 | | simplrl 800 |
. . . . . . . . . . . . 13
|
40 | | simprll 802 |
. . . . . . . . . . . . 13
|
41 | | llyi 21277 |
. . . . . . . . . . . . 13
Locally
SConn
↾t SConn |
42 | 38, 39, 40, 41 | mp3an2i 1429 |
. . . . . . . . . . . 12
↾t SConn |
43 | | simplrr 801 |
. . . . . . . . . . . . 13
|
44 | | simprlr 803 |
. . . . . . . . . . . . 13
|
45 | | llyi 21277 |
. . . . . . . . . . . . 13
Locally
SConn ↾t SConn |
46 | 38, 43, 44, 45 | mp3an2i 1429 |
. . . . . . . . . . . 12
↾t SConn |
47 | | reeanv 3107 |
. . . . . . . . . . . . 13
↾t SConn
↾t SConn
↾t SConn
↾t SConn |
48 | | simpl2 1065 |
. . . . . . . . . . . . . . . . . 18
↾t SConn
↾t SConn |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . 17
↾t SConn
↾t SConn |
50 | | simpr2 1068 |
. . . . . . . . . . . . . . . . . 18
↾t SConn
↾t SConn |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . 17
↾t SConn
↾t SConn |
52 | | simprl1 1106 |
. . . . . . . . . . . . . . . . . . . 20
↾t SConn
↾t SConn |
53 | | simprr1 1109 |
. . . . . . . . . . . . . . . . . . . 20
↾t SConn
↾t SConn
|
54 | | xpss12 5225 |
. . . . . . . . . . . . . . . . . . . 20
|
55 | 52, 53, 54 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
↾t SConn
↾t SConn
|
56 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . 19
↾t SConn
↾t SConn
|
57 | 55, 56 | sstrd 3613 |
. . . . . . . . . . . . . . . . . 18
↾t SConn
↾t SConn
|
58 | 57 | ex 450 |
. . . . . . . . . . . . . . . . 17
↾t SConn
↾t SConn |
59 | 49, 51, 58 | 3jcad 1243 |
. . . . . . . . . . . . . . . 16
↾t SConn
↾t SConn
|
60 | | simp3 1063 |
. . . . . . . . . . . . . . . . 17
↾t SConn
↾t SConn |
61 | | simp3 1063 |
. . . . . . . . . . . . . . . . 17
↾t SConn
↾t
SConn |
62 | 60, 61 | anim12i 590 |
. . . . . . . . . . . . . . . 16
↾t SConn
↾t SConn
↾t SConn ↾t SConn |
63 | 59, 62 | jca2 556 |
. . . . . . . . . . . . . . 15
↾t SConn
↾t SConn
↾t SConn
↾t SConn |
64 | 63 | reximdv 3016 |
. . . . . . . . . . . . . 14
↾t SConn
↾t SConn
↾t SConn
↾t
SConn |
65 | 64 | reximdv 3016 |
. . . . . . . . . . . . 13
↾t SConn
↾t SConn
↾t SConn
↾t
SConn |
66 | 47, 65 | syl5bir 233 |
. . . . . . . . . . . 12
↾t SConn
↾t SConn
↾t SConn
↾t
SConn |
67 | 42, 46, 66 | mp2and 715 |
. . . . . . . . . . 11
↾t SConn
↾t
SConn |
68 | 67 | ex 450 |
. . . . . . . . . 10
↾t SConn ↾t SConn |
69 | 68 | rexlimdvva 3038 |
. . . . . . . . 9
↾t SConn ↾t SConn |
70 | 37, 69 | mpd 15 |
. . . . . . . 8
↾t SConn
↾t
SConn |
71 | | simp3l1 1166 |
. . . . . . . . . . 11
↾t SConn
↾t
SConn
|
72 | | simp3l2 1167 |
. . . . . . . . . . 11
↾t SConn
↾t
SConn
|
73 | | cvmlift2.b |
. . . . . . . . . . . . 13
|
74 | | simpl1l 1112 |
. . . . . . . . . . . . . 14
↾t SConn
↾t
SConn
↾t
|
75 | 74, 1 | syl 17 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
CovMap |
76 | 74, 2 | syl 17 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
|
77 | | cvmlift2.p |
. . . . . . . . . . . . . 14
|
78 | 74, 77 | syl 17 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
|
79 | | cvmlift2.i |
. . . . . . . . . . . . . 14
|
80 | 74, 79 | syl 17 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
|
81 | | cvmlift2.h |
. . . . . . . . . . . . 13
|
82 | | cvmlift2.k |
. . . . . . . . . . . . 13
|
83 | | df-ov 6653 |
. . . . . . . . . . . . . 14
|
84 | | simpl1r 1113 |
. . . . . . . . . . . . . . 15
↾t SConn
↾t
SConn
↾t
|
85 | 84 | simpld 475 |
. . . . . . . . . . . . . 14
↾t SConn
↾t
SConn
↾t
|
86 | 83, 85 | syl5eqel 2705 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
|
87 | 84 | simprd 479 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
|
88 | | simpl2l 1114 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
|
89 | | simpl2r 1115 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
|
90 | | simp3rl 1134 |
. . . . . . . . . . . . . . 15
↾t SConn
↾t
SConn
↾t
SConn |
91 | 90 | adantr 481 |
. . . . . . . . . . . . . 14
↾t SConn
↾t
SConn
↾t
↾t SConn |
92 | | sconnpconn 31209 |
. . . . . . . . . . . . . 14
↾t SConn ↾t PConn |
93 | | pconnconn 31213 |
. . . . . . . . . . . . . 14
↾t PConn ↾t Conn |
94 | 91, 92, 93 | 3syl 18 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
↾t Conn |
95 | | simp3rr 1135 |
. . . . . . . . . . . . . . 15
↾t SConn
↾t
SConn
↾t
SConn |
96 | 95 | adantr 481 |
. . . . . . . . . . . . . 14
↾t SConn
↾t
SConn
↾t
↾t SConn |
97 | | sconnpconn 31209 |
. . . . . . . . . . . . . 14
↾t SConn ↾t PConn |
98 | | pconnconn 31213 |
. . . . . . . . . . . . . 14
↾t PConn ↾t Conn |
99 | 96, 97, 98 | 3syl 18 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
↾t Conn |
100 | 71 | adantr 481 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
|
101 | 72 | adantr 481 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
|
102 | | simp3l3 1168 |
. . . . . . . . . . . . . 14
↾t SConn
↾t
SConn
|
103 | 102 | adantr 481 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
|
104 | | simprl 794 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
|
105 | | simprr 796 |
. . . . . . . . . . . . 13
↾t SConn
↾t
SConn
↾t
↾t |
106 | | eqid 2622 |
. . . . . . . . . . . . 13
|
107 | 73, 75, 76, 78, 80, 81, 82, 13, 86, 87, 88, 89, 94, 99, 100, 101, 103, 104, 105, 106 | cvmlift2lem9 31293 |
. . . . . . . . . . . 12
↾t SConn
↾t
SConn
↾t
↾t |
108 | 107 | rexlimdvaa 3032 |
. . . . . . . . . . 11
↾t SConn
↾t
SConn
↾t
↾t |
109 | 71, 72, 108 | 3jca 1242 |
. . . . . . . . . 10
↾t SConn
↾t
SConn
↾t
↾t |
110 | 109 | 3expia 1267 |
. . . . . . . . 9
↾t SConn ↾t SConn
↾t
↾t |
111 | 110 | reximdvva 3019 |
. . . . . . . 8
↾t SConn ↾t SConn
↾t
↾t |
112 | 70, 111 | mpd 15 |
. . . . . . 7
↾t
↾t |
113 | 112 | expr 643 |
. . . . . 6
↾t
↾t |
114 | 113 | exlimdv 1861 |
. . . . 5
↾t
↾t |
115 | 16, 114 | syl5bi 232 |
. . . 4
↾t
↾t |
116 | 115 | expimpd 629 |
. . 3
↾t
↾t |
117 | 116 | rexlimdvw 3034 |
. 2
↾t
↾t |
118 | 15, 117 | mpd 15 |
1
↾t
↾t |