Step | Hyp | Ref
| Expression |
1 | | cvmtop1 31242 |
. . . . . 6
CovMap
|
2 | 1 | 3ad2ant1 1082 |
. . . . 5
CovMap
|
3 | | cvmcov.1 |
. . . . . . . 8
↾t
↾t |
4 | 3 | cvmsuni 31251 |
. . . . . . 7
|
5 | 4 | 3ad2ant2 1083 |
. . . . . 6
CovMap
|
6 | 3 | cvmsss 31249 |
. . . . . . . 8
|
7 | 6 | 3ad2ant2 1083 |
. . . . . . 7
CovMap
|
8 | 7 | unissd 4462 |
. . . . . 6
CovMap
|
9 | 5, 8 | eqsstr3d 3640 |
. . . . 5
CovMap
|
10 | | eqid 2622 |
. . . . . 6
|
11 | 10 | restuni 20966 |
. . . . 5
↾t |
12 | 2, 9, 11 | syl2anc 693 |
. . . 4
CovMap
↾t |
13 | 12 | difeq1d 3727 |
. . 3
CovMap
↾t |
14 | | unisng 4452 |
. . . . . . 7
|
15 | 14 | 3ad2ant3 1084 |
. . . . . 6
CovMap
|
16 | 15 | uneq2d 3767 |
. . . . 5
CovMap
|
17 | | uniun 4456 |
. . . . . 6
|
18 | | undif1 4043 |
. . . . . . . . 9
|
19 | | simp3 1063 |
. . . . . . . . . . 11
CovMap
|
20 | 19 | snssd 4340 |
. . . . . . . . . 10
CovMap
|
21 | | ssequn2 3786 |
. . . . . . . . . 10
|
22 | 20, 21 | sylib 208 |
. . . . . . . . 9
CovMap
|
23 | 18, 22 | syl5eq 2668 |
. . . . . . . 8
CovMap
|
24 | 23 | unieqd 4446 |
. . . . . . 7
CovMap
|
25 | 24, 5 | eqtrd 2656 |
. . . . . 6
CovMap
|
26 | 17, 25 | syl5eqr 2670 |
. . . . 5
CovMap
|
27 | 16, 26 | eqtr3d 2658 |
. . . 4
CovMap
|
28 | | difss 3737 |
. . . . . . 7
|
29 | 28 | unissi 4461 |
. . . . . 6
|
30 | 29, 5 | syl5sseq 3653 |
. . . . 5
CovMap
|
31 | | uniiun 4573 |
. . . . . . . 8
|
32 | 31 | ineq2i 3811 |
. . . . . . 7
|
33 | | incom 3805 |
. . . . . . 7
|
34 | | iunin2 4584 |
. . . . . . 7
|
35 | 32, 33, 34 | 3eqtr4i 2654 |
. . . . . 6
|
36 | | eldifsn 4317 |
. . . . . . . . . 10
|
37 | | nesym 2850 |
. . . . . . . . . . . 12
|
38 | 3 | cvmsdisj 31252 |
. . . . . . . . . . . . . 14
|
39 | 38 | 3expa 1265 |
. . . . . . . . . . . . 13
|
40 | 39 | ord 392 |
. . . . . . . . . . . 12
|
41 | 37, 40 | syl5bi 232 |
. . . . . . . . . . 11
|
42 | 41 | impr 649 |
. . . . . . . . . 10
|
43 | 36, 42 | sylan2b 492 |
. . . . . . . . 9
|
44 | 43 | iuneq2dv 4542 |
. . . . . . . 8
|
45 | 44 | 3adant1 1079 |
. . . . . . 7
CovMap
|
46 | | iun0 4576 |
. . . . . . 7
|
47 | 45, 46 | syl6eq 2672 |
. . . . . 6
CovMap
|
48 | 35, 47 | syl5eq 2668 |
. . . . 5
CovMap
|
49 | | uneqdifeq 4057 |
. . . . 5
|
50 | 30, 48, 49 | syl2anc 693 |
. . . 4
CovMap
|
51 | 27, 50 | mpbid 222 |
. . 3
CovMap
|
52 | 13, 51 | eqtr3d 2658 |
. 2
CovMap
↾t |
53 | | uniexg 6955 |
. . . . . 6
|
54 | 53 | 3ad2ant2 1083 |
. . . . 5
CovMap
|
55 | 5, 54 | eqeltrrd 2702 |
. . . 4
CovMap
|
56 | | resttop 20964 |
. . . 4
↾t |
57 | 2, 55, 56 | syl2anc 693 |
. . 3
CovMap
↾t |
58 | | elssuni 4467 |
. . . . . . . . . . 11
|
59 | 58 | adantl 482 |
. . . . . . . . . 10
CovMap
|
60 | 5 | adantr 481 |
. . . . . . . . . 10
CovMap
|
61 | 59, 60 | sseqtrd 3641 |
. . . . . . . . 9
CovMap
|
62 | | df-ss 3588 |
. . . . . . . . 9
|
63 | 61, 62 | sylib 208 |
. . . . . . . 8
CovMap
|
64 | 2 | adantr 481 |
. . . . . . . . 9
CovMap
|
65 | 55 | adantr 481 |
. . . . . . . . 9
CovMap
|
66 | 7 | sselda 3603 |
. . . . . . . . 9
CovMap
|
67 | | elrestr 16089 |
. . . . . . . . 9
↾t |
68 | 64, 65, 66, 67 | syl3anc 1326 |
. . . . . . . 8
CovMap
↾t |
69 | 63, 68 | eqeltrrd 2702 |
. . . . . . 7
CovMap
↾t |
70 | 69 | ex 450 |
. . . . . 6
CovMap
↾t |
71 | 70 | ssrdv 3609 |
. . . . 5
CovMap
↾t |
72 | 71 | ssdifssd 3748 |
. . . 4
CovMap
↾t |
73 | | uniopn 20702 |
. . . 4
↾t
↾t ↾t |
74 | 57, 72, 73 | syl2anc 693 |
. . 3
CovMap
↾t |
75 | | eqid 2622 |
. . . 4
↾t ↾t |
76 | 75 | opncld 20837 |
. . 3
↾t
↾t
↾t ↾t |
77 | 57, 74, 76 | syl2anc 693 |
. 2
CovMap
↾t ↾t |
78 | 52, 77 | eqeltrrd 2702 |
1
CovMap
↾t |