Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π¦ β π½) β π¦ β π½) |
2 | | neibastop1.4 |
. . . . . . . . . 10
β’ π½ = {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β
} |
3 | | ssrab2 4041 |
. . . . . . . . . 10
β’ {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β
} β π« π |
4 | 2, 3 | eqsstri 3982 |
. . . . . . . . 9
β’ π½ β π« π |
5 | 1, 4 | sstrdi 3960 |
. . . . . . . 8
β’ ((π β§ π¦ β π½) β π¦ β π« π) |
6 | | sspwuni 5064 |
. . . . . . . 8
β’ (π¦ β π« π β βͺ π¦
β π) |
7 | 5, 6 | sylib 217 |
. . . . . . 7
β’ ((π β§ π¦ β π½) β βͺ π¦ β π) |
8 | | vuniex 7680 |
. . . . . . . 8
β’ βͺ π¦
β V |
9 | 8 | elpw 4568 |
. . . . . . 7
β’ (βͺ π¦
β π« π β
βͺ π¦ β π) |
10 | 7, 9 | sylibr 233 |
. . . . . 6
β’ ((π β§ π¦ β π½) β βͺ π¦ β π« π) |
11 | | eluni2 4873 |
. . . . . . . 8
β’ (π₯ β βͺ π¦
β βπ§ β
π¦ π₯ β π§) |
12 | | elssuni 4902 |
. . . . . . . . . . . . 13
β’ (π§ β π¦ β π§ β βͺ π¦) |
13 | 12 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β π½) β§ (π§ β π¦ β§ π₯ β π§)) β π§ β βͺ π¦) |
14 | 13 | sspwd 4577 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β π½) β§ (π§ β π¦ β§ π₯ β π§)) β π« π§ β π« βͺ π¦) |
15 | | sslin 4198 |
. . . . . . . . . . 11
β’
(π« π§ β
π« βͺ π¦ β ((πΉβπ₯) β© π« π§) β ((πΉβπ₯) β© π« βͺ π¦)) |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π¦ β π½) β§ (π§ β π¦ β§ π₯ β π§)) β ((πΉβπ₯) β© π« π§) β ((πΉβπ₯) β© π« βͺ π¦)) |
17 | 1 | sselda 3948 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β π½) β§ π§ β π¦) β π§ β π½) |
18 | 17 | adantrr 716 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β π½) β§ (π§ β π¦ β§ π₯ β π§)) β π§ β π½) |
19 | | pweq 4578 |
. . . . . . . . . . . . . . . . 17
β’ (π = π§ β π« π = π« π§) |
20 | 19 | ineq2d 4176 |
. . . . . . . . . . . . . . . 16
β’ (π = π§ β ((πΉβπ₯) β© π« π) = ((πΉβπ₯) β© π« π§)) |
21 | 20 | neeq1d 3000 |
. . . . . . . . . . . . . . 15
β’ (π = π§ β (((πΉβπ₯) β© π« π) β β
β ((πΉβπ₯) β© π« π§) β β
)) |
22 | 21 | raleqbi1dv 3306 |
. . . . . . . . . . . . . 14
β’ (π = π§ β (βπ₯ β π ((πΉβπ₯) β© π« π) β β
β βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
)) |
23 | 22, 2 | elrab2 3652 |
. . . . . . . . . . . . 13
β’ (π§ β π½ β (π§ β π« π β§ βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
)) |
24 | 23 | simprbi 498 |
. . . . . . . . . . . 12
β’ (π§ β π½ β βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
) |
25 | 18, 24 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β π½) β§ (π§ β π¦ β§ π₯ β π§)) β βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
) |
26 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β π½) β§ (π§ β π¦ β§ π₯ β π§)) β π₯ β π§) |
27 | | rsp 3229 |
. . . . . . . . . . 11
β’
(βπ₯ β
π§ ((πΉβπ₯) β© π« π§) β β
β (π₯ β π§ β ((πΉβπ₯) β© π« π§) β β
)) |
28 | 25, 26, 27 | sylc 65 |
. . . . . . . . . 10
β’ (((π β§ π¦ β π½) β§ (π§ β π¦ β§ π₯ β π§)) β ((πΉβπ₯) β© π« π§) β β
) |
29 | | ssn0 4364 |
. . . . . . . . . 10
β’ ((((πΉβπ₯) β© π« π§) β ((πΉβπ₯) β© π« βͺ π¦)
β§ ((πΉβπ₯) β© π« π§) β β
) β ((πΉβπ₯) β© π« βͺ π¦)
β β
) |
30 | 16, 28, 29 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π¦ β π½) β§ (π§ β π¦ β§ π₯ β π§)) β ((πΉβπ₯) β© π« βͺ π¦)
β β
) |
31 | 30 | rexlimdvaa 3150 |
. . . . . . . 8
β’ ((π β§ π¦ β π½) β (βπ§ β π¦ π₯ β π§ β ((πΉβπ₯) β© π« βͺ π¦)
β β
)) |
32 | 11, 31 | biimtrid 241 |
. . . . . . 7
β’ ((π β§ π¦ β π½) β (π₯ β βͺ π¦ β ((πΉβπ₯) β© π« βͺ π¦)
β β
)) |
33 | 32 | ralrimiv 3139 |
. . . . . 6
β’ ((π β§ π¦ β π½) β βπ₯ β βͺ π¦((πΉβπ₯) β© π« βͺ π¦)
β β
) |
34 | | pweq 4578 |
. . . . . . . . . 10
β’ (π = βͺ
π¦ β π« π = π« βͺ π¦) |
35 | 34 | ineq2d 4176 |
. . . . . . . . 9
β’ (π = βͺ
π¦ β ((πΉβπ₯) β© π« π) = ((πΉβπ₯) β© π« βͺ π¦)) |
36 | 35 | neeq1d 3000 |
. . . . . . . 8
β’ (π = βͺ
π¦ β (((πΉβπ₯) β© π« π) β β
β ((πΉβπ₯) β© π« βͺ π¦)
β β
)) |
37 | 36 | raleqbi1dv 3306 |
. . . . . . 7
β’ (π = βͺ
π¦ β (βπ₯ β π ((πΉβπ₯) β© π« π) β β
β βπ₯ β βͺ π¦((πΉβπ₯) β© π« βͺ π¦)
β β
)) |
38 | 37, 2 | elrab2 3652 |
. . . . . 6
β’ (βͺ π¦
β π½ β (βͺ π¦
β π« π β§
βπ₯ β βͺ π¦((πΉβπ₯) β© π« βͺ π¦)
β β
)) |
39 | 10, 33, 38 | sylanbrc 584 |
. . . . 5
β’ ((π β§ π¦ β π½) β βͺ π¦ β π½) |
40 | 39 | ex 414 |
. . . 4
β’ (π β (π¦ β π½ β βͺ π¦ β π½)) |
41 | 40 | alrimiv 1931 |
. . 3
β’ (π β βπ¦(π¦ β π½ β βͺ π¦ β π½)) |
42 | | pweq 4578 |
. . . . . . . . . . 11
β’ (π = π¦ β π« π = π« π¦) |
43 | 42 | ineq2d 4176 |
. . . . . . . . . 10
β’ (π = π¦ β ((πΉβπ₯) β© π« π) = ((πΉβπ₯) β© π« π¦)) |
44 | 43 | neeq1d 3000 |
. . . . . . . . 9
β’ (π = π¦ β (((πΉβπ₯) β© π« π) β β
β ((πΉβπ₯) β© π« π¦) β β
)) |
45 | 44 | raleqbi1dv 3306 |
. . . . . . . 8
β’ (π = π¦ β (βπ₯ β π ((πΉβπ₯) β© π« π) β β
β βπ₯ β π¦ ((πΉβπ₯) β© π« π¦) β β
)) |
46 | 45, 2 | elrab2 3652 |
. . . . . . 7
β’ (π¦ β π½ β (π¦ β π« π β§ βπ₯ β π¦ ((πΉβπ₯) β© π« π¦) β β
)) |
47 | 46, 23 | anbi12i 628 |
. . . . . 6
β’ ((π¦ β π½ β§ π§ β π½) β ((π¦ β π« π β§ βπ₯ β π¦ ((πΉβπ₯) β© π« π¦) β β
) β§ (π§ β π« π β§ βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
))) |
48 | | an4 655 |
. . . . . 6
β’ (((π¦ β π« π β§ βπ₯ β π¦ ((πΉβπ₯) β© π« π¦) β β
) β§ (π§ β π« π β§ βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
)) β ((π¦ β π« π β§ π§ β π« π) β§ (βπ₯ β π¦ ((πΉβπ₯) β© π« π¦) β β
β§ βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
))) |
49 | 47, 48 | bitri 275 |
. . . . 5
β’ ((π¦ β π½ β§ π§ β π½) β ((π¦ β π« π β§ π§ β π« π) β§ (βπ₯ β π¦ ((πΉβπ₯) β© π« π¦) β β
β§ βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
))) |
50 | | inss1 4192 |
. . . . . . . . . 10
β’ (π¦ β© π§) β π¦ |
51 | | elpwi 4571 |
. . . . . . . . . 10
β’ (π¦ β π« π β π¦ β π) |
52 | 50, 51 | sstrid 3959 |
. . . . . . . . 9
β’ (π¦ β π« π β (π¦ β© π§) β π) |
53 | 52 | ad2antrl 727 |
. . . . . . . 8
β’ ((π β§ (π¦ β π« π β§ π§ β π« π)) β (π¦ β© π§) β π) |
54 | 53 | adantrr 716 |
. . . . . . 7
β’ ((π β§ ((π¦ β π« π β§ π§ β π« π) β§ (βπ₯ β π¦ ((πΉβπ₯) β© π« π¦) β β
β§ βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
))) β (π¦ β© π§) β π) |
55 | | vex 3451 |
. . . . . . . . 9
β’ π¦ β V |
56 | 55 | inex1 5278 |
. . . . . . . 8
β’ (π¦ β© π§) β V |
57 | 56 | elpw 4568 |
. . . . . . 7
β’ ((π¦ β© π§) β π« π β (π¦ β© π§) β π) |
58 | 54, 57 | sylibr 233 |
. . . . . 6
β’ ((π β§ ((π¦ β π« π β§ π§ β π« π) β§ (βπ₯ β π¦ ((πΉβπ₯) β© π« π¦) β β
β§ βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
))) β (π¦ β© π§) β π« π) |
59 | | ssralv 4014 |
. . . . . . . . . . 11
β’ ((π¦ β© π§) β π¦ β (βπ₯ β π¦ ((πΉβπ₯) β© π« π¦) β β
β βπ₯ β (π¦ β© π§)((πΉβπ₯) β© π« π¦) β β
)) |
60 | 50, 59 | ax-mp 5 |
. . . . . . . . . 10
β’
(βπ₯ β
π¦ ((πΉβπ₯) β© π« π¦) β β
β βπ₯ β (π¦ β© π§)((πΉβπ₯) β© π« π¦) β β
) |
61 | | inss2 4193 |
. . . . . . . . . . 11
β’ (π¦ β© π§) β π§ |
62 | | ssralv 4014 |
. . . . . . . . . . 11
β’ ((π¦ β© π§) β π§ β (βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
β βπ₯ β (π¦ β© π§)((πΉβπ₯) β© π« π§) β β
)) |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . . 10
β’
(βπ₯ β
π§ ((πΉβπ₯) β© π« π§) β β
β βπ₯ β (π¦ β© π§)((πΉβπ₯) β© π« π§) β β
) |
64 | 60, 63 | anim12i 614 |
. . . . . . . . 9
β’
((βπ₯ β
π¦ ((πΉβπ₯) β© π« π¦) β β
β§ βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
) β (βπ₯ β (π¦ β© π§)((πΉβπ₯) β© π« π¦) β β
β§ βπ₯ β (π¦ β© π§)((πΉβπ₯) β© π« π§) β β
)) |
65 | | r19.26 3111 |
. . . . . . . . 9
β’
(βπ₯ β
(π¦ β© π§)(((πΉβπ₯) β© π« π¦) β β
β§ ((πΉβπ₯) β© π« π§) β β
) β (βπ₯ β (π¦ β© π§)((πΉβπ₯) β© π« π¦) β β
β§ βπ₯ β (π¦ β© π§)((πΉβπ₯) β© π« π§) β β
)) |
66 | 64, 65 | sylibr 233 |
. . . . . . . 8
β’
((βπ₯ β
π¦ ((πΉβπ₯) β© π« π¦) β β
β§ βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
) β βπ₯ β (π¦ β© π§)(((πΉβπ₯) β© π« π¦) β β
β§ ((πΉβπ₯) β© π« π§) β β
)) |
67 | | n0 4310 |
. . . . . . . . . . 11
β’ (((πΉβπ₯) β© π« π¦) β β
β βπ£ π£ β ((πΉβπ₯) β© π« π¦)) |
68 | | n0 4310 |
. . . . . . . . . . 11
β’ (((πΉβπ₯) β© π« π§) β β
β βπ€ π€ β ((πΉβπ₯) β© π« π§)) |
69 | 67, 68 | anbi12i 628 |
. . . . . . . . . 10
β’ ((((πΉβπ₯) β© π« π¦) β β
β§ ((πΉβπ₯) β© π« π§) β β
) β (βπ£ π£ β ((πΉβπ₯) β© π« π¦) β§ βπ€ π€ β ((πΉβπ₯) β© π« π§))) |
70 | | exdistrv 1960 |
. . . . . . . . . . 11
β’
(βπ£βπ€(π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§)) β (βπ£ π£ β ((πΉβπ₯) β© π« π¦) β§ βπ€ π€ β ((πΉβπ₯) β© π« π§))) |
71 | | inss2 4193 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπ₯) β© π« π¦) β π« π¦ |
72 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β π£ β ((πΉβπ₯) β© π« π¦)) |
73 | 71, 72 | sselid 3946 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β π£ β π« π¦) |
74 | 73 | elpwid 4573 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β π£ β π¦) |
75 | | inss2 4193 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπ₯) β© π« π§) β π« π§ |
76 | | simprr 772 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β π€ β ((πΉβπ₯) β© π« π§)) |
77 | 75, 76 | sselid 3946 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β π€ β π« π§) |
78 | 77 | elpwid 4573 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β π€ β π§) |
79 | | ss2in 4200 |
. . . . . . . . . . . . . . . . 17
β’ ((π£ β π¦ β§ π€ β π§) β (π£ β© π€) β (π¦ β© π§)) |
80 | 74, 78, 79 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β (π£ β© π€) β (π¦ β© π§)) |
81 | 80 | sspwd 4577 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β π« (π£ β© π€) β π« (π¦ β© π§)) |
82 | | sslin 4198 |
. . . . . . . . . . . . . . 15
β’
(π« (π£ β©
π€) β π« (π¦ β© π§) β ((πΉβπ₯) β© π« (π£ β© π€)) β ((πΉβπ₯) β© π« (π¦ β© π§))) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β ((πΉβπ₯) β© π« (π£ β© π€)) β ((πΉβπ₯) β© π« (π¦ β© π§))) |
84 | | simplll 774 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β π) |
85 | 53 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β (π¦ β© π§) β π) |
86 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β π₯ β (π¦ β© π§)) |
87 | 85, 86 | sseldd 3949 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β π₯ β π) |
88 | | inss1 4192 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ₯) β© π« π¦) β (πΉβπ₯) |
89 | 88, 72 | sselid 3946 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β π£ β (πΉβπ₯)) |
90 | | inss1 4192 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ₯) β© π« π§) β (πΉβπ₯) |
91 | 90, 76 | sselid 3946 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β π€ β (πΉβπ₯)) |
92 | | neibastop1.3 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯) β§ π€ β (πΉβπ₯))) β ((πΉβπ₯) β© π« (π£ β© π€)) β β
) |
93 | 84, 87, 89, 91, 92 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β ((πΉβπ₯) β© π« (π£ β© π€)) β β
) |
94 | | ssn0 4364 |
. . . . . . . . . . . . . 14
β’ ((((πΉβπ₯) β© π« (π£ β© π€)) β ((πΉβπ₯) β© π« (π¦ β© π§)) β§ ((πΉβπ₯) β© π« (π£ β© π€)) β β
) β ((πΉβπ₯) β© π« (π¦ β© π§)) β β
) |
95 | 83, 93, 94 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β§ (π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§))) β ((πΉβπ₯) β© π« (π¦ β© π§)) β β
) |
96 | 95 | ex 414 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β ((π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§)) β ((πΉβπ₯) β© π« (π¦ β© π§)) β β
)) |
97 | 96 | exlimdvv 1938 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β (βπ£βπ€(π£ β ((πΉβπ₯) β© π« π¦) β§ π€ β ((πΉβπ₯) β© π« π§)) β ((πΉβπ₯) β© π« (π¦ β© π§)) β β
)) |
98 | 70, 97 | biimtrrid 242 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β ((βπ£ π£ β ((πΉβπ₯) β© π« π¦) β§ βπ€ π€ β ((πΉβπ₯) β© π« π§)) β ((πΉβπ₯) β© π« (π¦ β© π§)) β β
)) |
99 | 69, 98 | biimtrid 241 |
. . . . . . . . 9
β’ (((π β§ (π¦ β π« π β§ π§ β π« π)) β§ π₯ β (π¦ β© π§)) β ((((πΉβπ₯) β© π« π¦) β β
β§ ((πΉβπ₯) β© π« π§) β β
) β ((πΉβπ₯) β© π« (π¦ β© π§)) β β
)) |
100 | 99 | ralimdva 3161 |
. . . . . . . 8
β’ ((π β§ (π¦ β π« π β§ π§ β π« π)) β (βπ₯ β (π¦ β© π§)(((πΉβπ₯) β© π« π¦) β β
β§ ((πΉβπ₯) β© π« π§) β β
) β βπ₯ β (π¦ β© π§)((πΉβπ₯) β© π« (π¦ β© π§)) β β
)) |
101 | 66, 100 | syl5 34 |
. . . . . . 7
β’ ((π β§ (π¦ β π« π β§ π§ β π« π)) β ((βπ₯ β π¦ ((πΉβπ₯) β© π« π¦) β β
β§ βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
) β βπ₯ β (π¦ β© π§)((πΉβπ₯) β© π« (π¦ β© π§)) β β
)) |
102 | 101 | impr 456 |
. . . . . 6
β’ ((π β§ ((π¦ β π« π β§ π§ β π« π) β§ (βπ₯ β π¦ ((πΉβπ₯) β© π« π¦) β β
β§ βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
))) β βπ₯ β (π¦ β© π§)((πΉβπ₯) β© π« (π¦ β© π§)) β β
) |
103 | | pweq 4578 |
. . . . . . . . . 10
β’ (π = (π¦ β© π§) β π« π = π« (π¦ β© π§)) |
104 | 103 | ineq2d 4176 |
. . . . . . . . 9
β’ (π = (π¦ β© π§) β ((πΉβπ₯) β© π« π) = ((πΉβπ₯) β© π« (π¦ β© π§))) |
105 | 104 | neeq1d 3000 |
. . . . . . . 8
β’ (π = (π¦ β© π§) β (((πΉβπ₯) β© π« π) β β
β ((πΉβπ₯) β© π« (π¦ β© π§)) β β
)) |
106 | 105 | raleqbi1dv 3306 |
. . . . . . 7
β’ (π = (π¦ β© π§) β (βπ₯ β π ((πΉβπ₯) β© π« π) β β
β βπ₯ β (π¦ β© π§)((πΉβπ₯) β© π« (π¦ β© π§)) β β
)) |
107 | 106, 2 | elrab2 3652 |
. . . . . 6
β’ ((π¦ β© π§) β π½ β ((π¦ β© π§) β π« π β§ βπ₯ β (π¦ β© π§)((πΉβπ₯) β© π« (π¦ β© π§)) β β
)) |
108 | 58, 102, 107 | sylanbrc 584 |
. . . . 5
β’ ((π β§ ((π¦ β π« π β§ π§ β π« π) β§ (βπ₯ β π¦ ((πΉβπ₯) β© π« π¦) β β
β§ βπ₯ β π§ ((πΉβπ₯) β© π« π§) β β
))) β (π¦ β© π§) β π½) |
109 | 49, 108 | sylan2b 595 |
. . . 4
β’ ((π β§ (π¦ β π½ β§ π§ β π½)) β (π¦ β© π§) β π½) |
110 | 109 | ralrimivva 3194 |
. . 3
β’ (π β βπ¦ β π½ βπ§ β π½ (π¦ β© π§) β π½) |
111 | | neibastop1.1 |
. . . . . 6
β’ (π β π β π) |
112 | | sspwuni 5064 |
. . . . . . . 8
β’ (π½ β π« π β βͺ π½
β π) |
113 | 4, 112 | mpbi 229 |
. . . . . . 7
β’ βͺ π½
β π |
114 | 113 | a1i 11 |
. . . . . 6
β’ (π β βͺ π½
β π) |
115 | 111, 114 | ssexd 5285 |
. . . . 5
β’ (π β βͺ π½
β V) |
116 | | uniexb 7702 |
. . . . 5
β’ (π½ β V β βͺ π½
β V) |
117 | 115, 116 | sylibr 233 |
. . . 4
β’ (π β π½ β V) |
118 | | istopg 22267 |
. . . 4
β’ (π½ β V β (π½ β Top β
(βπ¦(π¦ β π½ β βͺ π¦ β π½) β§ βπ¦ β π½ βπ§ β π½ (π¦ β© π§) β π½))) |
119 | 117, 118 | syl 17 |
. . 3
β’ (π β (π½ β Top β (βπ¦(π¦ β π½ β βͺ π¦ β π½) β§ βπ¦ β π½ βπ§ β π½ (π¦ β© π§) β π½))) |
120 | 41, 110, 119 | mpbir2and 712 |
. 2
β’ (π β π½ β Top) |
121 | | pwidg 4584 |
. . . . . 6
β’ (π β π β π β π« π) |
122 | 111, 121 | syl 17 |
. . . . 5
β’ (π β π β π« π) |
123 | | neibastop1.2 |
. . . . . . . . . 10
β’ (π β πΉ:πβΆ(π« π« π β
{β
})) |
124 | 123 | ffvelcdmda 7039 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (πΉβπ₯) β (π« π« π β
{β
})) |
125 | | eldifi 4090 |
. . . . . . . . 9
β’ ((πΉβπ₯) β (π« π« π β {β
}) β
(πΉβπ₯) β π« π« π) |
126 | | elpwi 4571 |
. . . . . . . . 9
β’ ((πΉβπ₯) β π« π« π β (πΉβπ₯) β π« π) |
127 | 124, 125,
126 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (πΉβπ₯) β π« π) |
128 | | df-ss 3931 |
. . . . . . . 8
β’ ((πΉβπ₯) β π« π β ((πΉβπ₯) β© π« π) = (πΉβπ₯)) |
129 | 127, 128 | sylib 217 |
. . . . . . 7
β’ ((π β§ π₯ β π) β ((πΉβπ₯) β© π« π) = (πΉβπ₯)) |
130 | | eldifsni 4754 |
. . . . . . . 8
β’ ((πΉβπ₯) β (π« π« π β {β
}) β
(πΉβπ₯) β β
) |
131 | 124, 130 | syl 17 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (πΉβπ₯) β β
) |
132 | 129, 131 | eqnetrd 3008 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((πΉβπ₯) β© π« π) β β
) |
133 | 132 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ₯ β π ((πΉβπ₯) β© π« π) β β
) |
134 | | pweq 4578 |
. . . . . . . . 9
β’ (π = π β π« π = π« π) |
135 | 134 | ineq2d 4176 |
. . . . . . . 8
β’ (π = π β ((πΉβπ₯) β© π« π) = ((πΉβπ₯) β© π« π)) |
136 | 135 | neeq1d 3000 |
. . . . . . 7
β’ (π = π β (((πΉβπ₯) β© π« π) β β
β ((πΉβπ₯) β© π« π) β β
)) |
137 | 136 | raleqbi1dv 3306 |
. . . . . 6
β’ (π = π β (βπ₯ β π ((πΉβπ₯) β© π« π) β β
β βπ₯ β π ((πΉβπ₯) β© π« π) β β
)) |
138 | 137, 2 | elrab2 3652 |
. . . . 5
β’ (π β π½ β (π β π« π β§ βπ₯ β π ((πΉβπ₯) β© π« π) β β
)) |
139 | 122, 133,
138 | sylanbrc 584 |
. . . 4
β’ (π β π β π½) |
140 | | elssuni 4902 |
. . . 4
β’ (π β π½ β π β βͺ π½) |
141 | 139, 140 | syl 17 |
. . 3
β’ (π β π β βͺ π½) |
142 | 141, 114 | eqssd 3965 |
. 2
β’ (π β π = βͺ π½) |
143 | | istopon 22284 |
. 2
β’ (π½ β (TopOnβπ) β (π½ β Top β§ π = βͺ π½)) |
144 | 120, 142,
143 | sylanbrc 584 |
1
β’ (π β π½ β (TopOnβπ)) |