Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β π½ β (TopOnβπ)) |
2 | | filelss 23356 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ π β πΉ) β π β π) |
3 | 2 | 3adant1 1131 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β π β π) |
4 | | resttopon 22665 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π β π) β (π½ βΎt π) β (TopOnβπ)) |
5 | 1, 3, 4 | syl2anc 585 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (π½ βΎt π) β (TopOnβπ)) |
6 | | filfbas 23352 |
. . . . . . . 8
β’ (πΉ β (Filβπ) β πΉ β (fBasβπ)) |
7 | 6 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β πΉ β (fBasβπ)) |
8 | | simp3 1139 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β π β πΉ) |
9 | | fbncp 23343 |
. . . . . . 7
β’ ((πΉ β (fBasβπ) β§ π β πΉ) β Β¬ (π β π) β πΉ) |
10 | 7, 8, 9 | syl2anc 585 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β Β¬ (π β π) β πΉ) |
11 | | simp2 1138 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β πΉ β (Filβπ)) |
12 | | trfil3 23392 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ π β π) β ((πΉ βΎt π) β (Filβπ) β Β¬ (π β π) β πΉ)) |
13 | 11, 3, 12 | syl2anc 585 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β ((πΉ βΎt π) β (Filβπ) β Β¬ (π β π) β πΉ)) |
14 | 10, 13 | mpbird 257 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (πΉ βΎt π) β (Filβπ)) |
15 | | fclsopn 23518 |
. . . . 5
β’ (((π½ βΎt π) β (TopOnβπ) β§ (πΉ βΎt π) β (Filβπ)) β (π₯ β ((π½ βΎt π) fClus (πΉ βΎt π)) β (π₯ β π β§ βπ¦ β (π½ βΎt π)(π₯ β π¦ β βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
)))) |
16 | 5, 14, 15 | syl2anc 585 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (π₯ β ((π½ βΎt π) fClus (πΉ βΎt π)) β (π₯ β π β§ βπ¦ β (π½ βΎt π)(π₯ β π¦ β βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
)))) |
17 | | in32 4222 |
. . . . . . . . . . . . . 14
β’ ((π’ β© π ) β© π) = ((π’ β© π) β© π ) |
18 | | ineq2 4207 |
. . . . . . . . . . . . . 14
β’ (π = π‘ β ((π’ β© π) β© π ) = ((π’ β© π) β© π‘)) |
19 | 17, 18 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ (π = π‘ β ((π’ β© π ) β© π) = ((π’ β© π) β© π‘)) |
20 | 19 | neeq1d 3001 |
. . . . . . . . . . . 12
β’ (π = π‘ β (((π’ β© π ) β© π) β β
β ((π’ β© π) β© π‘) β β
)) |
21 | 20 | rspccv 3610 |
. . . . . . . . . . 11
β’
(βπ β
πΉ ((π’ β© π ) β© π) β β
β (π‘ β πΉ β ((π’ β© π) β© π‘) β β
)) |
22 | | inss1 4229 |
. . . . . . . . . . . . 13
β’ (π’ β© π) β π’ |
23 | | ssrin 4234 |
. . . . . . . . . . . . 13
β’ ((π’ β© π) β π’ β ((π’ β© π) β© π‘) β (π’ β© π‘)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((π’ β© π) β© π‘) β (π’ β© π‘) |
25 | | ssn0 4401 |
. . . . . . . . . . . 12
β’ ((((π’ β© π) β© π‘) β (π’ β© π‘) β§ ((π’ β© π) β© π‘) β β
) β (π’ β© π‘) β β
) |
26 | 24, 25 | mpan 689 |
. . . . . . . . . . 11
β’ (((π’ β© π) β© π‘) β β
β (π’ β© π‘) β β
) |
27 | 21, 26 | syl6 35 |
. . . . . . . . . 10
β’
(βπ β
πΉ ((π’ β© π ) β© π) β β
β (π‘ β πΉ β (π’ β© π‘) β β
)) |
28 | 27 | ralrimiv 3146 |
. . . . . . . . 9
β’
(βπ β
πΉ ((π’ β© π ) β© π) β β
β βπ‘ β πΉ (π’ β© π‘) β β
) |
29 | 11 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β§ π β πΉ) β πΉ β (Filβπ)) |
30 | | simpr 486 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β§ π β πΉ) β π β πΉ) |
31 | 8 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β§ π β πΉ) β π β πΉ) |
32 | | filin 23358 |
. . . . . . . . . . . 12
β’ ((πΉ β (Filβπ) β§ π β πΉ β§ π β πΉ) β (π β© π) β πΉ) |
33 | 29, 30, 31, 32 | syl3anc 1372 |
. . . . . . . . . . 11
β’
(((((π½ β
(TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β§ π β πΉ) β (π β© π) β πΉ) |
34 | | ineq2 4207 |
. . . . . . . . . . . . . 14
β’ (π‘ = (π β© π) β (π’ β© π‘) = (π’ β© (π β© π))) |
35 | | inass 4220 |
. . . . . . . . . . . . . 14
β’ ((π’ β© π ) β© π) = (π’ β© (π β© π)) |
36 | 34, 35 | eqtr4di 2791 |
. . . . . . . . . . . . 13
β’ (π‘ = (π β© π) β (π’ β© π‘) = ((π’ β© π ) β© π)) |
37 | 36 | neeq1d 3001 |
. . . . . . . . . . . 12
β’ (π‘ = (π β© π) β ((π’ β© π‘) β β
β ((π’ β© π ) β© π) β β
)) |
38 | 37 | rspcv 3609 |
. . . . . . . . . . 11
β’ ((π β© π) β πΉ β (βπ‘ β πΉ (π’ β© π‘) β β
β ((π’ β© π ) β© π) β β
)) |
39 | 33, 38 | syl 17 |
. . . . . . . . . 10
β’
(((((π½ β
(TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β§ π β πΉ) β (βπ‘ β πΉ (π’ β© π‘) β β
β ((π’ β© π ) β© π) β β
)) |
40 | 39 | ralrimdva 3155 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β (βπ‘ β πΉ (π’ β© π‘) β β
β βπ β πΉ ((π’ β© π ) β© π) β β
)) |
41 | 28, 40 | impbid2 225 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β (βπ β πΉ ((π’ β© π ) β© π) β β
β βπ‘ β πΉ (π’ β© π‘) β β
)) |
42 | 41 | imbi2d 341 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β ((π₯ β π’ β βπ β πΉ ((π’ β© π ) β© π) β β
) β (π₯ β π’ β βπ‘ β πΉ (π’ β© π‘) β β
))) |
43 | 42 | ralbidva 3176 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (βπ’ β π½ (π₯ β π’ β βπ β πΉ ((π’ β© π ) β© π) β β
) β βπ’ β π½ (π₯ β π’ β βπ‘ β πΉ (π’ β© π‘) β β
))) |
44 | | vex 3479 |
. . . . . . . . 9
β’ π’ β V |
45 | 44 | inex1 5318 |
. . . . . . . 8
β’ (π’ β© π) β V |
46 | 45 | a1i 11 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π’ β π½) β (π’ β© π) β V) |
47 | | elrest 17373 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ π β πΉ) β (π¦ β (π½ βΎt π) β βπ’ β π½ π¦ = (π’ β© π))) |
48 | 47 | 3adant2 1132 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (π¦ β (π½ βΎt π) β βπ’ β π½ π¦ = (π’ β© π))) |
49 | 48 | adantr 482 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (π¦ β (π½ βΎt π) β βπ’ β π½ π¦ = (π’ β© π))) |
50 | | eleq2 2823 |
. . . . . . . . 9
β’ (π¦ = (π’ β© π) β (π₯ β π¦ β π₯ β (π’ β© π))) |
51 | | elin 3965 |
. . . . . . . . . . 11
β’ (π₯ β (π’ β© π) β (π₯ β π’ β§ π₯ β π)) |
52 | 51 | rbaib 540 |
. . . . . . . . . 10
β’ (π₯ β π β (π₯ β (π’ β© π) β π₯ β π’)) |
53 | 52 | adantl 483 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (π₯ β (π’ β© π) β π₯ β π’)) |
54 | 50, 53 | sylan9bbr 512 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π¦ = (π’ β© π)) β (π₯ β π¦ β π₯ β π’)) |
55 | | vex 3479 |
. . . . . . . . . . . 12
β’ π β V |
56 | 55 | inex1 5318 |
. . . . . . . . . . 11
β’ (π β© π) β V |
57 | 56 | a1i 11 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π β πΉ) β (π β© π) β V) |
58 | | elrest 17373 |
. . . . . . . . . . . 12
β’ ((πΉ β (Filβπ) β§ π β πΉ) β (π§ β (πΉ βΎt π) β βπ β πΉ π§ = (π β© π))) |
59 | 58 | 3adant1 1131 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (π§ β (πΉ βΎt π) β βπ β πΉ π§ = (π β© π))) |
60 | 59 | adantr 482 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (π§ β (πΉ βΎt π) β βπ β πΉ π§ = (π β© π))) |
61 | | ineq2 4207 |
. . . . . . . . . . . 12
β’ (π§ = (π β© π) β (π¦ β© π§) = (π¦ β© (π β© π))) |
62 | 61 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π§ = (π β© π)) β (π¦ β© π§) = (π¦ β© (π β© π))) |
63 | 62 | neeq1d 3001 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π§ = (π β© π)) β ((π¦ β© π§) β β
β (π¦ β© (π β© π)) β β
)) |
64 | 57, 60, 63 | ralxfr2d 5409 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
β βπ β πΉ (π¦ β© (π β© π)) β β
)) |
65 | | ineq1 4206 |
. . . . . . . . . . . 12
β’ (π¦ = (π’ β© π) β (π¦ β© (π β© π)) = ((π’ β© π) β© (π β© π))) |
66 | | inindir 4228 |
. . . . . . . . . . . 12
β’ ((π’ β© π ) β© π) = ((π’ β© π) β© (π β© π)) |
67 | 65, 66 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π¦ = (π’ β© π) β (π¦ β© (π β© π)) = ((π’ β© π ) β© π)) |
68 | 67 | neeq1d 3001 |
. . . . . . . . . 10
β’ (π¦ = (π’ β© π) β ((π¦ β© (π β© π)) β β
β ((π’ β© π ) β© π) β β
)) |
69 | 68 | ralbidv 3178 |
. . . . . . . . 9
β’ (π¦ = (π’ β© π) β (βπ β πΉ (π¦ β© (π β© π)) β β
β βπ β πΉ ((π’ β© π ) β© π) β β
)) |
70 | 64, 69 | sylan9bb 511 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π¦ = (π’ β© π)) β (βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
β βπ β πΉ ((π’ β© π ) β© π) β β
)) |
71 | 54, 70 | imbi12d 345 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β§ π¦ = (π’ β© π)) β ((π₯ β π¦ β βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
) β (π₯ β π’ β βπ β πΉ ((π’ β© π ) β© π) β β
))) |
72 | 46, 49, 71 | ralxfr2d 5409 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (βπ¦ β (π½ βΎt π)(π₯ β π¦ β βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
) β βπ’ β π½ (π₯ β π’ β βπ β πΉ ((π’ β© π ) β© π) β β
))) |
73 | 1 | adantr 482 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β π½ β (TopOnβπ)) |
74 | 11 | adantr 482 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β πΉ β (Filβπ)) |
75 | 3 | sselda 3983 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β π₯ β π) |
76 | | fclsopn 23518 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π₯ β (π½ fClus πΉ) β (π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ‘ β πΉ (π’ β© π‘) β β
)))) |
77 | 76 | baibd 541 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π₯ β π) β (π₯ β (π½ fClus πΉ) β βπ’ β π½ (π₯ β π’ β βπ‘ β πΉ (π’ β© π‘) β β
))) |
78 | 73, 74, 75, 77 | syl21anc 837 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (π₯ β (π½ fClus πΉ) β βπ’ β π½ (π₯ β π’ β βπ‘ β πΉ (π’ β© π‘) β β
))) |
79 | 43, 72, 78 | 3bitr4d 311 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ π₯ β π) β (βπ¦ β (π½ βΎt π)(π₯ β π¦ β βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
) β π₯ β (π½ fClus πΉ))) |
80 | 79 | pm5.32da 580 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β ((π₯ β π β§ βπ¦ β (π½ βΎt π)(π₯ β π¦ β βπ§ β (πΉ βΎt π)(π¦ β© π§) β β
)) β (π₯ β π β§ π₯ β (π½ fClus πΉ)))) |
81 | 16, 80 | bitrd 279 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (π₯ β ((π½ βΎt π) fClus (πΉ βΎt π)) β (π₯ β π β§ π₯ β (π½ fClus πΉ)))) |
82 | | elin 3965 |
. . . 4
β’ (π₯ β ((π½ fClus πΉ) β© π) β (π₯ β (π½ fClus πΉ) β§ π₯ β π)) |
83 | 82 | biancomi 464 |
. . 3
β’ (π₯ β ((π½ fClus πΉ) β© π) β (π₯ β π β§ π₯ β (π½ fClus πΉ))) |
84 | 81, 83 | bitr4di 289 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (π₯ β ((π½ βΎt π) fClus (πΉ βΎt π)) β π₯ β ((π½ fClus πΉ) β© π))) |
85 | 84 | eqrdv 2731 |
1
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β ((π½ βΎt π) fClus (πΉ βΎt π)) = ((π½ fClus πΉ) β© π)) |