Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β π½ β (TopOnβπ)) |
2 | | filelss 23363 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ π β πΉ) β π β π) |
3 | 2 | 3adant1 1130 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β π β π) |
4 | | resttopon 22672 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π β π) β (π½ βΎt π) β (TopOnβπ)) |
5 | 1, 3, 4 | syl2anc 584 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (π½ βΎt π) β (TopOnβπ)) |
6 | | filfbas 23359 |
. . . . . . . 8
β’ (πΉ β (Filβπ) β πΉ β (fBasβπ)) |
7 | 6 | 3ad2ant2 1134 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β πΉ β (fBasβπ)) |
8 | | simp3 1138 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β π β πΉ) |
9 | | fbncp 23350 |
. . . . . . 7
β’ ((πΉ β (fBasβπ) β§ π β πΉ) β Β¬ (π β π) β πΉ) |
10 | 7, 8, 9 | syl2anc 584 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β Β¬ (π β π) β πΉ) |
11 | | simp2 1137 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β πΉ β (Filβπ)) |
12 | | trfil3 23399 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ π β π) β ((πΉ βΎt π) β (Filβπ) β Β¬ (π β π) β πΉ)) |
13 | 11, 3, 12 | syl2anc 584 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β ((πΉ βΎt π) β (Filβπ) β Β¬ (π β π) β πΉ)) |
14 | 10, 13 | mpbird 256 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (πΉ βΎt π) β (Filβπ)) |
15 | | fclsopn 23525 |
. . . . 5
β’ (((π½ βΎt π) β (TopOnβπ) β§ (πΉ βΎt π) β (Filβπ)) β (π₯ β ((π½ βΎt π) fClus (πΉ βΎt π)) β (π₯ β π β§ βπ¦ β (π½ βΎt π)(π₯ β π¦ β βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
)))) |
16 | 5, 14, 15 | syl2anc 584 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (π₯ β ((π½ βΎt π) fClus (πΉ βΎt π)) β (π₯ β π β§ βπ¦ β (π½ βΎt π)(π₯ β π¦ β βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
)))) |
17 | | in32 4221 |
. . . . . . . . . . . . . 14
β’ ((π’ β© π ) β© π) = ((π’ β© π) β© π ) |
18 | | ineq2 4206 |
. . . . . . . . . . . . . 14
β’ (π = π‘ β ((π’ β© π) β© π ) = ((π’ β© π) β© π‘)) |
19 | 17, 18 | eqtrid 2784 |
. . . . . . . . . . . . 13
β’ (π = π‘ β ((π’ β© π ) β© π) = ((π’ β© π) β© π‘)) |
20 | 19 | neeq1d 3000 |
. . . . . . . . . . . 12
β’ (π = π‘ β (((π’ β© π ) β© π) β β
β ((π’ β© π) β© π‘) β β
)) |
21 | 20 | rspccv 3609 |
. . . . . . . . . . 11
β’
(βπ β
πΉ ((π’ β© π ) β© π) β β
β (π‘ β πΉ β ((π’ β© π) β© π‘) β β
)) |
22 | | inss1 4228 |
. . . . . . . . . . . . 13
β’ (π’ β© π) β π’ |
23 | | ssrin 4233 |
. . . . . . . . . . . . 13
β’ ((π’ β© π) β π’ β ((π’ β© π) β© π‘) β (π’ β© π‘)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((π’ β© π) β© π‘) β (π’ β© π‘) |
25 | | ssn0 4400 |
. . . . . . . . . . . 12
β’ ((((π’ β© π) β© π‘) β (π’ β© π‘) β§ ((π’ β© π) β© π‘) β β
) β (π’ β© π‘) β β
) |
26 | 24, 25 | mpan 688 |
. . . . . . . . . . 11
β’ (((π’ β© π) β© π‘) β β
β (π’ β© π‘) β β
) |
27 | 21, 26 | syl6 35 |
. . . . . . . . . 10
β’
(βπ β
πΉ ((π’ β© π ) β© π) β β
β (π‘ β πΉ β (π’ β© π‘) β β
)) |
28 | 27 | ralrimiv 3145 |
. . . . . . . . 9
β’
(βπ β
πΉ ((π’ β© π ) β© π) β β
β βπ‘ β πΉ (π’ β© π‘) β β
) |
29 | 11 | ad3antrrr 728 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β§ π β πΉ) β πΉ β (Filβπ)) |
30 | | simpr 485 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β§ π β πΉ) β π β πΉ) |
31 | 8 | ad3antrrr 728 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β§ π β πΉ) β π β πΉ) |
32 | | filin 23365 |
. . . . . . . . . . . 12
β’ ((πΉ β (Filβπ) β§ π β πΉ β§ π β πΉ) β (π β© π) β πΉ) |
33 | 29, 30, 31, 32 | syl3anc 1371 |
. . . . . . . . . . 11
β’
(((((π½ β
(TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β§ π β πΉ) β (π β© π) β πΉ) |
34 | | ineq2 4206 |
. . . . . . . . . . . . . 14
β’ (π‘ = (π β© π) β (π’ β© π‘) = (π’ β© (π β© π))) |
35 | | inass 4219 |
. . . . . . . . . . . . . 14
β’ ((π’ β© π ) β© π) = (π’ β© (π β© π)) |
36 | 34, 35 | eqtr4di 2790 |
. . . . . . . . . . . . 13
β’ (π‘ = (π β© π) β (π’ β© π‘) = ((π’ β© π ) β© π)) |
37 | 36 | neeq1d 3000 |
. . . . . . . . . . . 12
β’ (π‘ = (π β© π) β ((π’ β© π‘) β β
β ((π’ β© π ) β© π) β β
)) |
38 | 37 | rspcv 3608 |
. . . . . . . . . . 11
β’ ((π β© π) β πΉ β (βπ‘ β πΉ (π’ β© π‘) β β
β ((π’ β© π ) β© π) β β
)) |
39 | 33, 38 | syl 17 |
. . . . . . . . . 10
β’
(((((π½ β
(TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β§ π β πΉ) β (βπ‘ β πΉ (π’ β© π‘) β β
β ((π’ β© π ) β© π) β β
)) |
40 | 39 | ralrimdva 3154 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β (βπ‘ β πΉ (π’ β© π‘) β β
β βπ β πΉ ((π’ β© π ) β© π) β β
)) |
41 | 28, 40 | impbid2 225 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β (βπ β πΉ ((π’ β© π ) β© π) β β
β βπ‘ β πΉ (π’ β© π‘) β β
)) |
42 | 41 | imbi2d 340 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β ((π₯ β π’ β βπ β πΉ ((π’ β© π ) β© π) β β
) β (π₯ β π’ β βπ‘ β πΉ (π’ β© π‘) β β
))) |
43 | 42 | ralbidva 3175 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (βπ’ β π½ (π₯ β π’ β βπ β πΉ ((π’ β© π ) β© π) β β
) β βπ’ β π½ (π₯ β π’ β βπ‘ β πΉ (π’ β© π‘) β β
))) |
44 | | vex 3478 |
. . . . . . . . 9
β’ π’ β V |
45 | 44 | inex1 5317 |
. . . . . . . 8
β’ (π’ β© π) β V |
46 | 45 | a1i 11 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β (π’ β© π) β V) |
47 | | elrest 17375 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ π β πΉ) β (π¦ β (π½ βΎt π) β βπ’ β π½ π¦ = (π’ β© π))) |
48 | 47 | 3adant2 1131 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (π¦ β (π½ βΎt π) β βπ’ β π½ π¦ = (π’ β© π))) |
49 | 48 | adantr 481 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (π¦ β (π½ βΎt π) β βπ’ β π½ π¦ = (π’ β© π))) |
50 | | eleq2 2822 |
. . . . . . . . 9
β’ (π¦ = (π’ β© π) β (π₯ β π¦ β π₯ β (π’ β© π))) |
51 | | elin 3964 |
. . . . . . . . . . 11
β’ (π₯ β (π’ β© π) β (π₯ β π’ β§ π₯ β π)) |
52 | 51 | rbaib 539 |
. . . . . . . . . 10
β’ (π₯ β π β (π₯ β (π’ β© π) β π₯ β π’)) |
53 | 52 | adantl 482 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (π₯ β (π’ β© π) β π₯ β π’)) |
54 | 50, 53 | sylan9bbr 511 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π¦ = (π’ β© π)) β (π₯ β π¦ β π₯ β π’)) |
55 | | vex 3478 |
. . . . . . . . . . . 12
β’ π β V |
56 | 55 | inex1 5317 |
. . . . . . . . . . 11
β’ (π β© π) β V |
57 | 56 | a1i 11 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π β πΉ) β (π β© π) β V) |
58 | | elrest 17375 |
. . . . . . . . . . . 12
β’ ((πΉ β (Filβπ) β§ π β πΉ) β (π§ β (πΉ βΎt π) β βπ β πΉ π§ = (π β© π))) |
59 | 58 | 3adant1 1130 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (π§ β (πΉ βΎt π) β βπ β πΉ π§ = (π β© π))) |
60 | 59 | adantr 481 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (π§ β (πΉ βΎt π) β βπ β πΉ π§ = (π β© π))) |
61 | | ineq2 4206 |
. . . . . . . . . . . 12
β’ (π§ = (π β© π) β (π¦ β© π§) = (π¦ β© (π β© π))) |
62 | 61 | adantl 482 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π§ = (π β© π)) β (π¦ β© π§) = (π¦ β© (π β© π))) |
63 | 62 | neeq1d 3000 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π§ = (π β© π)) β ((π¦ β© π§) β β
β (π¦ β© (π β© π)) β β
)) |
64 | 57, 60, 63 | ralxfr2d 5408 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
β βπ β πΉ (π¦ β© (π β© π)) β β
)) |
65 | | ineq1 4205 |
. . . . . . . . . . . 12
β’ (π¦ = (π’ β© π) β (π¦ β© (π β© π)) = ((π’ β© π) β© (π β© π))) |
66 | | inindir 4227 |
. . . . . . . . . . . 12
β’ ((π’ β© π ) β© π) = ((π’ β© π) β© (π β© π)) |
67 | 65, 66 | eqtr4di 2790 |
. . . . . . . . . . 11
β’ (π¦ = (π’ β© π) β (π¦ β© (π β© π)) = ((π’ β© π ) β© π)) |
68 | 67 | neeq1d 3000 |
. . . . . . . . . 10
β’ (π¦ = (π’ β© π) β ((π¦ β© (π β© π)) β β
β ((π’ β© π ) β© π) β β
)) |
69 | 68 | ralbidv 3177 |
. . . . . . . . 9
β’ (π¦ = (π’ β© π) β (βπ β πΉ (π¦ β© (π β© π)) β β
β βπ β πΉ ((π’ β© π ) β© π) β β
)) |
70 | 64, 69 | sylan9bb 510 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π¦ = (π’ β© π)) β (βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
β βπ β πΉ ((π’ β© π ) β© π) β β
)) |
71 | 54, 70 | imbi12d 344 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π¦ = (π’ β© π)) β ((π₯ β π¦ β βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
) β (π₯ β π’ β βπ β πΉ ((π’ β© π ) β© π) β β
))) |
72 | 46, 49, 71 | ralxfr2d 5408 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (βπ¦ β (π½ βΎt π)(π₯ β π¦ β βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
) β βπ’ β π½ (π₯ β π’ β βπ β πΉ ((π’ β© π ) β© π) β β
))) |
73 | 1 | adantr 481 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β π½ β (TopOnβπ)) |
74 | 11 | adantr 481 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β πΉ β (Filβπ)) |
75 | 3 | sselda 3982 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β π₯ β π) |
76 | | fclsopn 23525 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π₯ β (π½ fClus πΉ) β (π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ‘ β πΉ (π’ β© π‘) β β
)))) |
77 | 76 | baibd 540 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π₯ β π) β (π₯ β (π½ fClus πΉ) β βπ’ β π½ (π₯ β π’ β βπ‘ β πΉ (π’ β© π‘) β β
))) |
78 | 73, 74, 75, 77 | syl21anc 836 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (π₯ β (π½ fClus πΉ) β βπ’ β π½ (π₯ β π’ β βπ‘ β πΉ (π’ β© π‘) β β
))) |
79 | 43, 72, 78 | 3bitr4d 310 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (βπ¦ β (π½ βΎt π)(π₯ β π¦ β βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
) β π₯ β (π½ fClus πΉ))) |
80 | 79 | pm5.32da 579 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β ((π₯ β π β§ βπ¦ β (π½ βΎt π)(π₯ β π¦ β βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
)) β (π₯ β π β§ π₯ β (π½ fClus πΉ)))) |
81 | 16, 80 | bitrd 278 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (π₯ β ((π½ βΎt π) fClus (πΉ βΎt π)) β (π₯ β π β§ π₯ β (π½ fClus πΉ)))) |
82 | | elin 3964 |
. . . 4
β’ (π₯ β ((π½ fClus πΉ) β© π) β (π₯ β (π½ fClus πΉ) β§ π₯ β π)) |
83 | 82 | biancomi 463 |
. . 3
β’ (π₯ β ((π½ fClus πΉ) β© π) β (π₯ β π β§ π₯ β (π½ fClus πΉ))) |
84 | 81, 83 | bitr4di 288 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (π₯ β ((π½ βΎt π) fClus (πΉ βΎt π)) β π₯ β ((π½ fClus πΉ) β© π))) |
85 | 84 | eqrdv 2730 |
1
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β ((π½ βΎt π) fClus (πΉ βΎt π)) = ((π½ fClus πΉ) β© π)) |