Step | Hyp | Ref
| Expression |
1 | | filnet.h |
. . . . 5
β’ π» = βͺ π β πΉ ({π} Γ π) |
2 | | filnet.d |
. . . . 5
β’ π· = {β¨π₯, π¦β© β£ ((π₯ β π» β§ π¦ β π») β§ (1st βπ¦) β (1st
βπ₯))} |
3 | 1, 2 | filnetlem3 34855 |
. . . 4
β’ (π» = βͺ
βͺ π· β§ (πΉ β (Filβπ) β (π» β (πΉ Γ π) β§ π· β DirRel))) |
4 | 3 | simpri 487 |
. . 3
β’ (πΉ β (Filβπ) β (π» β (πΉ Γ π) β§ π· β DirRel)) |
5 | 4 | simprd 497 |
. 2
β’ (πΉ β (Filβπ) β π· β DirRel) |
6 | | f2ndres 7947 |
. . . . 5
β’
(2nd βΎ (πΉ Γ π)):(πΉ Γ π)βΆπ |
7 | 4 | simpld 496 |
. . . . 5
β’ (πΉ β (Filβπ) β π» β (πΉ Γ π)) |
8 | | fssres2 6711 |
. . . . 5
β’
(((2nd βΎ (πΉ Γ π)):(πΉ Γ π)βΆπ β§ π» β (πΉ Γ π)) β (2nd βΎ π»):π»βΆπ) |
9 | 6, 7, 8 | sylancr 588 |
. . . 4
β’ (πΉ β (Filβπ) β (2nd βΎ
π»):π»βΆπ) |
10 | | filtop 23209 |
. . . . . 6
β’ (πΉ β (Filβπ) β π β πΉ) |
11 | | xpexg 7685 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ π β πΉ) β (πΉ Γ π) β V) |
12 | 10, 11 | mpdan 686 |
. . . . 5
β’ (πΉ β (Filβπ) β (πΉ Γ π) β V) |
13 | 12, 7 | ssexd 5282 |
. . . 4
β’ (πΉ β (Filβπ) β π» β V) |
14 | 9, 13 | fexd 7178 |
. . 3
β’ (πΉ β (Filβπ) β (2nd βΎ
π») β
V) |
15 | 3 | simpli 485 |
. . . . . . 7
β’ π» = βͺ
βͺ π· |
16 | | dirdm 18490 |
. . . . . . . 8
β’ (π· β DirRel β dom π· = βͺ
βͺ π·) |
17 | 5, 16 | syl 17 |
. . . . . . 7
β’ (πΉ β (Filβπ) β dom π· = βͺ βͺ π·) |
18 | 15, 17 | eqtr4id 2796 |
. . . . . 6
β’ (πΉ β (Filβπ) β π» = dom π·) |
19 | 18 | feq2d 6655 |
. . . . 5
β’ (πΉ β (Filβπ) β ((2nd
βΎ π»):π»βΆπ β (2nd βΎ π»):dom π·βΆπ)) |
20 | 9, 19 | mpbid 231 |
. . . 4
β’ (πΉ β (Filβπ) β (2nd βΎ
π»):dom π·βΆπ) |
21 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ dom π· = dom π· |
22 | 21 | tailf 34850 |
. . . . . . . . . . . . 13
β’ (π· β DirRel β
(tailβπ·):dom π·βΆπ« dom π·) |
23 | 5, 22 | syl 17 |
. . . . . . . . . . . 12
β’ (πΉ β (Filβπ) β (tailβπ·):dom π·βΆπ« dom π·) |
24 | 18 | feq2d 6655 |
. . . . . . . . . . . 12
β’ (πΉ β (Filβπ) β ((tailβπ·):π»βΆπ« dom π· β (tailβπ·):dom π·βΆπ« dom π·)) |
25 | 23, 24 | mpbird 257 |
. . . . . . . . . . 11
β’ (πΉ β (Filβπ) β (tailβπ·):π»βΆπ« dom π·) |
26 | 25 | adantr 482 |
. . . . . . . . . 10
β’ ((πΉ β (Filβπ) β§ π‘ β π) β (tailβπ·):π»βΆπ« dom π·) |
27 | | ffn 6669 |
. . . . . . . . . 10
β’
((tailβπ·):π»βΆπ« dom π· β (tailβπ·) Fn π») |
28 | | imaeq2 6010 |
. . . . . . . . . . . 12
β’ (π = ((tailβπ·)βπ) β ((2nd βΎ π») β π) = ((2nd βΎ π») β ((tailβπ·)βπ))) |
29 | 28 | sseq1d 3976 |
. . . . . . . . . . 11
β’ (π = ((tailβπ·)βπ) β (((2nd βΎ π») β π) β π‘ β ((2nd βΎ π») β ((tailβπ·)βπ)) β π‘)) |
30 | 29 | rexrn 7038 |
. . . . . . . . . 10
β’
((tailβπ·) Fn
π» β (βπ β ran (tailβπ·)((2nd βΎ π») β π) β π‘ β βπ β π» ((2nd βΎ π») β ((tailβπ·)βπ)) β π‘)) |
31 | 26, 27, 30 | 3syl 18 |
. . . . . . . . 9
β’ ((πΉ β (Filβπ) β§ π‘ β π) β (βπ β ran (tailβπ·)((2nd βΎ π») β π) β π‘ β βπ β π» ((2nd βΎ π») β ((tailβπ·)βπ)) β π‘)) |
32 | | fo2nd 7943 |
. . . . . . . . . . . . . . 15
β’
2nd :VβontoβV |
33 | | fofn 6759 |
. . . . . . . . . . . . . . 15
β’
(2nd :VβontoβV β 2nd Fn V) |
34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
2nd Fn V |
35 | | ssv 3969 |
. . . . . . . . . . . . . 14
β’ π» β V |
36 | | fnssres 6625 |
. . . . . . . . . . . . . 14
β’
((2nd Fn V β§ π» β V) β (2nd βΎ
π») Fn π») |
37 | 34, 35, 36 | mp2an 691 |
. . . . . . . . . . . . 13
β’
(2nd βΎ π») Fn π» |
38 | | fnfun 6603 |
. . . . . . . . . . . . 13
β’
((2nd βΎ π») Fn π» β Fun (2nd βΎ π»)) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . 12
β’ Fun
(2nd βΎ π») |
40 | 26 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β ((tailβπ·)βπ) β π« dom π·) |
41 | 40 | elpwid 4570 |
. . . . . . . . . . . . . 14
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β ((tailβπ·)βπ) β dom π·) |
42 | 18 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β π» = dom π·) |
43 | 41, 42 | sseqtrrd 3986 |
. . . . . . . . . . . . 13
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β ((tailβπ·)βπ) β π») |
44 | 37 | fndmi 6607 |
. . . . . . . . . . . . 13
β’ dom
(2nd βΎ π»)
= π» |
45 | 43, 44 | sseqtrrdi 3996 |
. . . . . . . . . . . 12
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β ((tailβπ·)βπ) β dom (2nd βΎ π»)) |
46 | | funimass4 6908 |
. . . . . . . . . . . 12
β’ ((Fun
(2nd βΎ π»)
β§ ((tailβπ·)βπ) β dom (2nd βΎ π»)) β (((2nd
βΎ π») β
((tailβπ·)βπ)) β π‘ β βπ β ((tailβπ·)βπ)((2nd βΎ π»)βπ) β π‘)) |
47 | 39, 45, 46 | sylancr 588 |
. . . . . . . . . . 11
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β (((2nd βΎ π») β ((tailβπ·)βπ)) β π‘ β βπ β ((tailβπ·)βπ)((2nd βΎ π»)βπ) β π‘)) |
48 | 5 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β π· β DirRel) |
49 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β π β π») |
50 | 49, 42 | eleqtrd 2840 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β π β dom π·) |
51 | | vex 3450 |
. . . . . . . . . . . . . . . . 17
β’ π β V |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β π β V) |
53 | 21 | eltail 34849 |
. . . . . . . . . . . . . . . 16
β’ ((π· β DirRel β§ π β dom π· β§ π β V) β (π β ((tailβπ·)βπ) β ππ·π)) |
54 | 48, 50, 52, 53 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β (π β ((tailβπ·)βπ) β ππ·π)) |
55 | 49 | biantrurd 534 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β (π β π» β (π β π» β§ π β π»))) |
56 | 55 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β ((π β π» β§ (1st βπ) β (1st
βπ)) β ((π β π» β§ π β π») β§ (1st βπ) β (1st
βπ)))) |
57 | | vex 3450 |
. . . . . . . . . . . . . . . . 17
β’ π β V |
58 | 1, 2, 57, 51 | filnetlem1 34853 |
. . . . . . . . . . . . . . . 16
β’ (ππ·π β ((π β π» β§ π β π») β§ (1st βπ) β (1st
βπ))) |
59 | 56, 58 | bitr4di 289 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β ((π β π» β§ (1st βπ) β (1st
βπ)) β ππ·π)) |
60 | 54, 59 | bitr4d 282 |
. . . . . . . . . . . . . 14
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β (π β ((tailβπ·)βπ) β (π β π» β§ (1st βπ) β (1st
βπ)))) |
61 | 60 | imbi1d 342 |
. . . . . . . . . . . . 13
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β ((π β ((tailβπ·)βπ) β ((2nd βΎ π»)βπ) β π‘) β ((π β π» β§ (1st βπ) β (1st
βπ)) β
((2nd βΎ π»)βπ) β π‘))) |
62 | | fvres 6862 |
. . . . . . . . . . . . . . . . 17
β’ (π β π» β ((2nd βΎ π»)βπ) = (2nd βπ)) |
63 | 62 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
β’ (π β π» β (((2nd βΎ π»)βπ) β π‘ β (2nd βπ) β π‘)) |
64 | 63 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β π» β§ (1st βπ) β (1st
βπ)) β
(((2nd βΎ π»)βπ) β π‘ β (2nd βπ) β π‘)) |
65 | 64 | pm5.74i 271 |
. . . . . . . . . . . . . 14
β’ (((π β π» β§ (1st βπ) β (1st
βπ)) β
((2nd βΎ π»)βπ) β π‘) β ((π β π» β§ (1st βπ) β (1st
βπ)) β
(2nd βπ)
β π‘)) |
66 | | impexp 452 |
. . . . . . . . . . . . . 14
β’ (((π β π» β§ (1st βπ) β (1st
βπ)) β
(2nd βπ)
β π‘) β (π β π» β ((1st βπ) β (1st
βπ) β
(2nd βπ)
β π‘))) |
67 | 65, 66 | bitri 275 |
. . . . . . . . . . . . 13
β’ (((π β π» β§ (1st βπ) β (1st
βπ)) β
((2nd βΎ π»)βπ) β π‘) β (π β π» β ((1st βπ) β (1st
βπ) β
(2nd βπ)
β π‘))) |
68 | 61, 67 | bitrdi 287 |
. . . . . . . . . . . 12
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β ((π β ((tailβπ·)βπ) β ((2nd βΎ π»)βπ) β π‘) β (π β π» β ((1st βπ) β (1st
βπ) β
(2nd βπ)
β π‘)))) |
69 | 68 | ralbidv2 3171 |
. . . . . . . . . . 11
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β (βπ β ((tailβπ·)βπ)((2nd βΎ π»)βπ) β π‘ β βπ β π» ((1st βπ) β (1st βπ) β (2nd
βπ) β π‘))) |
70 | 47, 69 | bitrd 279 |
. . . . . . . . . 10
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β π») β (((2nd βΎ π») β ((tailβπ·)βπ)) β π‘ β βπ β π» ((1st βπ) β (1st βπ) β (2nd
βπ) β π‘))) |
71 | 70 | rexbidva 3174 |
. . . . . . . . 9
β’ ((πΉ β (Filβπ) β§ π‘ β π) β (βπ β π» ((2nd βΎ π») β ((tailβπ·)βπ)) β π‘ β βπ β π» βπ β π» ((1st βπ) β (1st βπ) β (2nd
βπ) β π‘))) |
72 | | vex 3450 |
. . . . . . . . . . . . . . . . 17
β’ π β V |
73 | | vex 3450 |
. . . . . . . . . . . . . . . . 17
β’ π£ β V |
74 | 72, 73 | op1std 7932 |
. . . . . . . . . . . . . . . 16
β’ (π = β¨π, π£β© β (1st βπ) = π) |
75 | 74 | sseq1d 3976 |
. . . . . . . . . . . . . . 15
β’ (π = β¨π, π£β© β ((1st βπ) β (1st
βπ) β π β (1st
βπ))) |
76 | 72, 73 | op2ndd 7933 |
. . . . . . . . . . . . . . . 16
β’ (π = β¨π, π£β© β (2nd βπ) = π£) |
77 | 76 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
β’ (π = β¨π, π£β© β ((2nd βπ) β π‘ β π£ β π‘)) |
78 | 75, 77 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π = β¨π, π£β© β (((1st βπ) β (1st
βπ) β
(2nd βπ)
β π‘) β (π β (1st
βπ) β π£ β π‘))) |
79 | 78 | raliunxp 5796 |
. . . . . . . . . . . . 13
β’
(βπ β
βͺ π β πΉ ({π} Γ π)((1st βπ) β (1st βπ) β (2nd
βπ) β π‘) β βπ β πΉ βπ£ β π (π β (1st βπ) β π£ β π‘)) |
80 | | sneq 4597 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β {π} = {π}) |
81 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β π = π) |
82 | 80, 81 | xpeq12d 5665 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ({π} Γ π) = ({π} Γ π)) |
83 | 82 | cbviunv 5001 |
. . . . . . . . . . . . . . 15
β’ βͺ π β πΉ ({π} Γ π) = βͺ π β πΉ ({π} Γ π) |
84 | 1, 83 | eqtri 2765 |
. . . . . . . . . . . . . 14
β’ π» = βͺ π β πΉ ({π} Γ π) |
85 | 84 | raleqi 3312 |
. . . . . . . . . . . . 13
β’
(βπ β
π» ((1st
βπ) β
(1st βπ)
β (2nd βπ) β π‘) β βπ β βͺ
π β πΉ ({π} Γ π)((1st βπ) β (1st βπ) β (2nd
βπ) β π‘)) |
86 | | dfss3 3933 |
. . . . . . . . . . . . . . . 16
β’ (π β π‘ β βπ£ β π π£ β π‘) |
87 | 86 | imbi2i 336 |
. . . . . . . . . . . . . . 15
β’ ((π β (1st
βπ) β π β π‘) β (π β (1st βπ) β βπ£ β π π£ β π‘)) |
88 | | r19.21v 3177 |
. . . . . . . . . . . . . . 15
β’
(βπ£ β
π (π β (1st βπ) β π£ β π‘) β (π β (1st βπ) β βπ£ β π π£ β π‘)) |
89 | 87, 88 | bitr4i 278 |
. . . . . . . . . . . . . 14
β’ ((π β (1st
βπ) β π β π‘) β βπ£ β π (π β (1st βπ) β π£ β π‘)) |
90 | 89 | ralbii 3097 |
. . . . . . . . . . . . 13
β’
(βπ β
πΉ (π β (1st βπ) β π β π‘) β βπ β πΉ βπ£ β π (π β (1st βπ) β π£ β π‘)) |
91 | 79, 85, 90 | 3bitr4i 303 |
. . . . . . . . . . . 12
β’
(βπ β
π» ((1st
βπ) β
(1st βπ)
β (2nd βπ) β π‘) β βπ β πΉ (π β (1st βπ) β π β π‘)) |
92 | 91 | rexbii 3098 |
. . . . . . . . . . 11
β’
(βπ β
π» βπ β π» ((1st βπ) β (1st βπ) β (2nd
βπ) β π‘) β βπ β π» βπ β πΉ (π β (1st βπ) β π β π‘)) |
93 | 1 | rexeqi 3313 |
. . . . . . . . . . 11
β’
(βπ β
π» βπ β πΉ (π β (1st βπ) β π β π‘) β βπ β βͺ
π β πΉ ({π} Γ π)βπ β πΉ (π β (1st βπ) β π β π‘)) |
94 | | vex 3450 |
. . . . . . . . . . . . . . . 16
β’ π β V |
95 | | vex 3450 |
. . . . . . . . . . . . . . . 16
β’ π β V |
96 | 94, 95 | op1std 7932 |
. . . . . . . . . . . . . . 15
β’ (π = β¨π, πβ© β (1st βπ) = π) |
97 | 96 | sseq2d 3977 |
. . . . . . . . . . . . . 14
β’ (π = β¨π, πβ© β (π β (1st βπ) β π β π)) |
98 | 97 | imbi1d 342 |
. . . . . . . . . . . . 13
β’ (π = β¨π, πβ© β ((π β (1st βπ) β π β π‘) β (π β π β π β π‘))) |
99 | 98 | ralbidv 3175 |
. . . . . . . . . . . 12
β’ (π = β¨π, πβ© β (βπ β πΉ (π β (1st βπ) β π β π‘) β βπ β πΉ (π β π β π β π‘))) |
100 | 99 | rexiunxp 5797 |
. . . . . . . . . . 11
β’
(βπ β
βͺ π β πΉ ({π} Γ π)βπ β πΉ (π β (1st βπ) β π β π‘) β βπ β πΉ βπ β π βπ β πΉ (π β π β π β π‘)) |
101 | 92, 93, 100 | 3bitri 297 |
. . . . . . . . . 10
β’
(βπ β
π» βπ β π» ((1st βπ) β (1st βπ) β (2nd
βπ) β π‘) β βπ β πΉ βπ β π βπ β πΉ (π β π β π β π‘)) |
102 | | fileln0 23204 |
. . . . . . . . . . . . . 14
β’ ((πΉ β (Filβπ) β§ π β πΉ) β π β β
) |
103 | 102 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β πΉ) β π β β
) |
104 | | r19.9rzv 4458 |
. . . . . . . . . . . . 13
β’ (π β β
β
(βπ β πΉ (π β π β π β π‘) β βπ β π βπ β πΉ (π β π β π β π‘))) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . 12
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β πΉ) β (βπ β πΉ (π β π β π β π‘) β βπ β π βπ β πΉ (π β π β π β π‘))) |
106 | | ssid 3967 |
. . . . . . . . . . . . . . 15
β’ π β π |
107 | | sseq1 3970 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β π β π β π)) |
108 | | sseq1 3970 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β π‘ β π β π‘)) |
109 | 107, 108 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π β π β π β π‘) β (π β π β π β π‘))) |
110 | 109 | rspcv 3578 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ β (βπ β πΉ (π β π β π β π‘) β (π β π β π β π‘))) |
111 | 106, 110 | mpii 46 |
. . . . . . . . . . . . . 14
β’ (π β πΉ β (βπ β πΉ (π β π β π β π‘) β π β π‘)) |
112 | 111 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β πΉ) β (βπ β πΉ (π β π β π β π‘) β π β π‘)) |
113 | | sstr2 3952 |
. . . . . . . . . . . . . . 15
β’ (π β π β (π β π‘ β π β π‘)) |
114 | 113 | com12 32 |
. . . . . . . . . . . . . 14
β’ (π β π‘ β (π β π β π β π‘)) |
115 | 114 | ralrimivw 3148 |
. . . . . . . . . . . . 13
β’ (π β π‘ β βπ β πΉ (π β π β π β π‘)) |
116 | 112, 115 | impbid1 224 |
. . . . . . . . . . . 12
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β πΉ) β (βπ β πΉ (π β π β π β π‘) β π β π‘)) |
117 | 105, 116 | bitr3d 281 |
. . . . . . . . . . 11
β’ (((πΉ β (Filβπ) β§ π‘ β π) β§ π β πΉ) β (βπ β π βπ β πΉ (π β π β π β π‘) β π β π‘)) |
118 | 117 | rexbidva 3174 |
. . . . . . . . . 10
β’ ((πΉ β (Filβπ) β§ π‘ β π) β (βπ β πΉ βπ β π βπ β πΉ (π β π β π β π‘) β βπ β πΉ π β π‘)) |
119 | 101, 118 | bitrid 283 |
. . . . . . . . 9
β’ ((πΉ β (Filβπ) β§ π‘ β π) β (βπ β π» βπ β π» ((1st βπ) β (1st βπ) β (2nd
βπ) β π‘) β βπ β πΉ π β π‘)) |
120 | 31, 71, 119 | 3bitrd 305 |
. . . . . . . 8
β’ ((πΉ β (Filβπ) β§ π‘ β π) β (βπ β ran (tailβπ·)((2nd βΎ π») β π) β π‘ β βπ β πΉ π β π‘)) |
121 | 120 | pm5.32da 580 |
. . . . . . 7
β’ (πΉ β (Filβπ) β ((π‘ β π β§ βπ β ran (tailβπ·)((2nd βΎ π») β π) β π‘) β (π‘ β π β§ βπ β πΉ π β π‘))) |
122 | | filn0 23216 |
. . . . . . . . . . . 12
β’ (πΉ β (Filβπ) β πΉ β β
) |
123 | 94 | snnz 4738 |
. . . . . . . . . . . . . . . 16
β’ {π} β β
|
124 | 102, 123 | jctil 521 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β (Filβπ) β§ π β πΉ) β ({π} β β
β§ π β β
)) |
125 | | neanior 3038 |
. . . . . . . . . . . . . . 15
β’ (({π} β β
β§ π β β
) β Β¬
({π} = β
β¨ π = β
)) |
126 | 124, 125 | sylib 217 |
. . . . . . . . . . . . . 14
β’ ((πΉ β (Filβπ) β§ π β πΉ) β Β¬ ({π} = β
β¨ π = β
)) |
127 | | ss0b 4358 |
. . . . . . . . . . . . . . 15
β’ (({π} Γ π) β β
β ({π} Γ π) = β
) |
128 | | xpeq0 6113 |
. . . . . . . . . . . . . . 15
β’ (({π} Γ π) = β
β ({π} = β
β¨ π = β
)) |
129 | 127, 128 | bitri 275 |
. . . . . . . . . . . . . 14
β’ (({π} Γ π) β β
β ({π} = β
β¨ π = β
)) |
130 | 126, 129 | sylnibr 329 |
. . . . . . . . . . . . 13
β’ ((πΉ β (Filβπ) β§ π β πΉ) β Β¬ ({π} Γ π) β β
) |
131 | 130 | ralrimiva 3144 |
. . . . . . . . . . . 12
β’ (πΉ β (Filβπ) β βπ β πΉ Β¬ ({π} Γ π) β β
) |
132 | | r19.2z 4453 |
. . . . . . . . . . . 12
β’ ((πΉ β β
β§
βπ β πΉ Β¬ ({π} Γ π) β β
) β βπ β πΉ Β¬ ({π} Γ π) β β
) |
133 | 122, 131,
132 | syl2anc 585 |
. . . . . . . . . . 11
β’ (πΉ β (Filβπ) β βπ β πΉ Β¬ ({π} Γ π) β β
) |
134 | | rexnal 3104 |
. . . . . . . . . . 11
β’
(βπ β
πΉ Β¬ ({π} Γ π) β β
β Β¬ βπ β πΉ ({π} Γ π) β β
) |
135 | 133, 134 | sylib 217 |
. . . . . . . . . 10
β’ (πΉ β (Filβπ) β Β¬ βπ β πΉ ({π} Γ π) β β
) |
136 | 1 | sseq1i 3973 |
. . . . . . . . . . . 12
β’ (π» β β
β βͺ π β πΉ ({π} Γ π) β β
) |
137 | | ss0b 4358 |
. . . . . . . . . . . 12
β’ (π» β β
β π» = β
) |
138 | | iunss 5006 |
. . . . . . . . . . . 12
β’ (βͺ π β πΉ ({π} Γ π) β β
β βπ β πΉ ({π} Γ π) β β
) |
139 | 136, 137,
138 | 3bitr3i 301 |
. . . . . . . . . . 11
β’ (π» = β
β βπ β πΉ ({π} Γ π) β β
) |
140 | 139 | necon3abii 2991 |
. . . . . . . . . 10
β’ (π» β β
β Β¬
βπ β πΉ ({π} Γ π) β β
) |
141 | 135, 140 | sylibr 233 |
. . . . . . . . 9
β’ (πΉ β (Filβπ) β π» β β
) |
142 | | dmresi 6006 |
. . . . . . . . . . . 12
β’ dom ( I
βΎ π») = π» |
143 | 1, 2 | filnetlem2 34854 |
. . . . . . . . . . . . . 14
β’ (( I
βΎ π») β π· β§ π· β (π» Γ π»)) |
144 | 143 | simpli 485 |
. . . . . . . . . . . . 13
β’ ( I
βΎ π») β π· |
145 | | dmss 5859 |
. . . . . . . . . . . . 13
β’ (( I
βΎ π») β π· β dom ( I βΎ π») β dom π·) |
146 | 144, 145 | ax-mp 5 |
. . . . . . . . . . . 12
β’ dom ( I
βΎ π») β dom
π· |
147 | 142, 146 | eqsstrri 3980 |
. . . . . . . . . . 11
β’ π» β dom π· |
148 | 143 | simpri 487 |
. . . . . . . . . . . . 13
β’ π· β (π» Γ π») |
149 | | dmss 5859 |
. . . . . . . . . . . . 13
β’ (π· β (π» Γ π») β dom π· β dom (π» Γ π»)) |
150 | 148, 149 | ax-mp 5 |
. . . . . . . . . . . 12
β’ dom π· β dom (π» Γ π») |
151 | | dmxpid 5886 |
. . . . . . . . . . . 12
β’ dom
(π» Γ π») = π» |
152 | 150, 151 | sseqtri 3981 |
. . . . . . . . . . 11
β’ dom π· β π» |
153 | 147, 152 | eqssi 3961 |
. . . . . . . . . 10
β’ π» = dom π· |
154 | 153 | tailfb 34852 |
. . . . . . . . 9
β’ ((π· β DirRel β§ π» β β
) β ran
(tailβπ·) β
(fBasβπ»)) |
155 | 5, 141, 154 | syl2anc 585 |
. . . . . . . 8
β’ (πΉ β (Filβπ) β ran (tailβπ·) β (fBasβπ»)) |
156 | | elfm 23301 |
. . . . . . . 8
β’ ((π β πΉ β§ ran (tailβπ·) β (fBasβπ») β§ (2nd βΎ π»):π»βΆπ) β (π‘ β ((π FilMap (2nd βΎ π»))βran (tailβπ·)) β (π‘ β π β§ βπ β ran (tailβπ·)((2nd βΎ π») β π) β π‘))) |
157 | 10, 155, 9, 156 | syl3anc 1372 |
. . . . . . 7
β’ (πΉ β (Filβπ) β (π‘ β ((π FilMap (2nd βΎ π»))βran (tailβπ·)) β (π‘ β π β§ βπ β ran (tailβπ·)((2nd βΎ π») β π) β π‘))) |
158 | | filfbas 23202 |
. . . . . . . 8
β’ (πΉ β (Filβπ) β πΉ β (fBasβπ)) |
159 | | elfg 23225 |
. . . . . . . 8
β’ (πΉ β (fBasβπ) β (π‘ β (πfilGenπΉ) β (π‘ β π β§ βπ β πΉ π β π‘))) |
160 | 158, 159 | syl 17 |
. . . . . . 7
β’ (πΉ β (Filβπ) β (π‘ β (πfilGenπΉ) β (π‘ β π β§ βπ β πΉ π β π‘))) |
161 | 121, 157,
160 | 3bitr4d 311 |
. . . . . 6
β’ (πΉ β (Filβπ) β (π‘ β ((π FilMap (2nd βΎ π»))βran (tailβπ·)) β π‘ β (πfilGenπΉ))) |
162 | 161 | eqrdv 2735 |
. . . . 5
β’ (πΉ β (Filβπ) β ((π FilMap (2nd βΎ π»))βran (tailβπ·)) = (πfilGenπΉ)) |
163 | | fgfil 23229 |
. . . . 5
β’ (πΉ β (Filβπ) β (πfilGenπΉ) = πΉ) |
164 | 162, 163 | eqtr2d 2778 |
. . . 4
β’ (πΉ β (Filβπ) β πΉ = ((π FilMap (2nd βΎ π»))βran (tailβπ·))) |
165 | 20, 164 | jca 513 |
. . 3
β’ (πΉ β (Filβπ) β ((2nd
βΎ π»):dom π·βΆπ β§ πΉ = ((π FilMap (2nd βΎ π»))βran (tailβπ·)))) |
166 | | feq1 6650 |
. . . . 5
β’ (π = (2nd βΎ π») β (π:dom π·βΆπ β (2nd βΎ π»):dom π·βΆπ)) |
167 | | oveq2 7366 |
. . . . . . 7
β’ (π = (2nd βΎ π») β (π FilMap π) = (π FilMap (2nd βΎ π»))) |
168 | 167 | fveq1d 6845 |
. . . . . 6
β’ (π = (2nd βΎ π») β ((π FilMap π)βran (tailβπ·)) = ((π FilMap (2nd βΎ π»))βran (tailβπ·))) |
169 | 168 | eqeq2d 2748 |
. . . . 5
β’ (π = (2nd βΎ π») β (πΉ = ((π FilMap π)βran (tailβπ·)) β πΉ = ((π FilMap (2nd βΎ π»))βran (tailβπ·)))) |
170 | 166, 169 | anbi12d 632 |
. . . 4
β’ (π = (2nd βΎ π») β ((π:dom π·βΆπ β§ πΉ = ((π FilMap π)βran (tailβπ·))) β ((2nd βΎ π»):dom π·βΆπ β§ πΉ = ((π FilMap (2nd βΎ π»))βran (tailβπ·))))) |
171 | 170 | spcegv 3557 |
. . 3
β’
((2nd βΎ π») β V β (((2nd βΎ
π»):dom π·βΆπ β§ πΉ = ((π FilMap (2nd βΎ π»))βran (tailβπ·))) β βπ(π:dom π·βΆπ β§ πΉ = ((π FilMap π)βran (tailβπ·))))) |
172 | 14, 165, 171 | sylc 65 |
. 2
β’ (πΉ β (Filβπ) β βπ(π:dom π·βΆπ β§ πΉ = ((π FilMap π)βran (tailβπ·)))) |
173 | | dmeq 5860 |
. . . . . 6
β’ (π = π· β dom π = dom π·) |
174 | 173 | feq2d 6655 |
. . . . 5
β’ (π = π· β (π:dom πβΆπ β π:dom π·βΆπ)) |
175 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π· β (tailβπ) = (tailβπ·)) |
176 | 175 | rneqd 5894 |
. . . . . . 7
β’ (π = π· β ran (tailβπ) = ran (tailβπ·)) |
177 | 176 | fveq2d 6847 |
. . . . . 6
β’ (π = π· β ((π FilMap π)βran (tailβπ)) = ((π FilMap π)βran (tailβπ·))) |
178 | 177 | eqeq2d 2748 |
. . . . 5
β’ (π = π· β (πΉ = ((π FilMap π)βran (tailβπ)) β πΉ = ((π FilMap π)βran (tailβπ·)))) |
179 | 174, 178 | anbi12d 632 |
. . . 4
β’ (π = π· β ((π:dom πβΆπ β§ πΉ = ((π FilMap π)βran (tailβπ))) β (π:dom π·βΆπ β§ πΉ = ((π FilMap π)βran (tailβπ·))))) |
180 | 179 | exbidv 1925 |
. . 3
β’ (π = π· β (βπ(π:dom πβΆπ β§ πΉ = ((π FilMap π)βran (tailβπ))) β βπ(π:dom π·βΆπ β§ πΉ = ((π FilMap π)βran (tailβπ·))))) |
181 | 180 | rspcev 3582 |
. 2
β’ ((π· β DirRel β§
βπ(π:dom π·βΆπ β§ πΉ = ((π FilMap π)βran (tailβπ·)))) β βπ β DirRel βπ(π:dom πβΆπ β§ πΉ = ((π FilMap π)βran (tailβπ)))) |
182 | 5, 172, 181 | syl2anc 585 |
1
β’ (πΉ β (Filβπ) β βπ β DirRel βπ(π:dom πβΆπ β§ πΉ = ((π FilMap π)βran (tailβπ)))) |