Step | Hyp | Ref
| Expression |
1 | | ssel 3942 |
. . . . . . . . . . . . 13
β’ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
(π€ β π¦ β π€ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ
{β
}))) |
2 | | elun 4113 |
. . . . . . . . . . . . . . 15
β’ (π€ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
(π€ β {π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β¨ π€ β {β
})) |
3 | | sseq2 3975 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = π€ β (π β π§ β π β π€)) |
4 | | pweq 4579 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ = π€ β π« π§ = π« π€) |
5 | 4 | ineq1d 4176 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = π€ β (π« π§ β© Fin) = (π« π€ β© Fin)) |
6 | 5 | raleqdv 3316 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = π€ β (βπ β (π« π§ β© Fin) Β¬ π = βͺ π β βπ β (π« π€ β© Fin) Β¬ π = βͺ
π)) |
7 | 3, 6 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π€ β ((π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π) β (π β π€ β§ βπ β (π« π€ β© Fin) Β¬ π = βͺ π))) |
8 | 7 | elrab 3650 |
. . . . . . . . . . . . . . . 16
β’ (π€ β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β (π€ β π« (fiβπ₯) β§ (π β π€ β§ βπ β (π« π€ β© Fin) Β¬ π = βͺ π))) |
9 | | velsn 4607 |
. . . . . . . . . . . . . . . 16
β’ (π€ β {β
} β π€ = β
) |
10 | 8, 9 | orbi12i 914 |
. . . . . . . . . . . . . . 15
β’ ((π€ β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β¨ π€ β {β
}) β ((π€ β π«
(fiβπ₯) β§ (π β π€ β§ βπ β (π« π€ β© Fin) Β¬ π = βͺ π)) β¨ π€ = β
)) |
11 | 2, 10 | bitri 275 |
. . . . . . . . . . . . . 14
β’ (π€ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
((π€ β π«
(fiβπ₯) β§ (π β π€ β§ βπ β (π« π€ β© Fin) Β¬ π = βͺ π)) β¨ π€ = β
)) |
12 | | elpwi 4572 |
. . . . . . . . . . . . . . . 16
β’ (π€ β π«
(fiβπ₯) β π€ β (fiβπ₯)) |
13 | 12 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π€ β π«
(fiβπ₯) β§ (π β π€ β§ βπ β (π« π€ β© Fin) Β¬ π = βͺ π)) β π€ β (fiβπ₯)) |
14 | | 0ss 4361 |
. . . . . . . . . . . . . . . 16
β’ β
β (fiβπ₯) |
15 | | sseq1 3974 |
. . . . . . . . . . . . . . . 16
β’ (π€ = β
β (π€ β (fiβπ₯) β β
β
(fiβπ₯))) |
16 | 14, 15 | mpbiri 258 |
. . . . . . . . . . . . . . 15
β’ (π€ = β
β π€ β (fiβπ₯)) |
17 | 13, 16 | jaoi 856 |
. . . . . . . . . . . . . 14
β’ (((π€ β π«
(fiβπ₯) β§ (π β π€ β§ βπ β (π« π€ β© Fin) Β¬ π = βͺ π)) β¨ π€ = β
) β π€ β (fiβπ₯)) |
18 | 11, 17 | sylbi 216 |
. . . . . . . . . . . . 13
β’ (π€ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β π€ β (fiβπ₯)) |
19 | 1, 18 | syl6 35 |
. . . . . . . . . . . 12
β’ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
(π€ β π¦ β π€ β (fiβπ₯))) |
20 | 19 | ralrimiv 3143 |
. . . . . . . . . . 11
β’ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
βπ€ β π¦ π€ β (fiβπ₯)) |
21 | | unissb 4905 |
. . . . . . . . . . 11
β’ (βͺ π¦
β (fiβπ₯) β
βπ€ β π¦ π€ β (fiβπ₯)) |
22 | 20, 21 | sylibr 233 |
. . . . . . . . . 10
β’ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β βͺ π¦
β (fiβπ₯)) |
23 | 22 | adantr 482 |
. . . . . . . . 9
β’ ((π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦)
β βͺ π¦ β (fiβπ₯)) |
24 | 23 | ad2antlr 726 |
. . . . . . . 8
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ Β¬ βͺ π¦ = β
) β βͺ π¦
β (fiβπ₯)) |
25 | | vuniex 7681 |
. . . . . . . . 9
β’ βͺ π¦
β V |
26 | 25 | elpw 4569 |
. . . . . . . 8
β’ (βͺ π¦
β π« (fiβπ₯) β βͺ π¦ β (fiβπ₯)) |
27 | 24, 26 | sylibr 233 |
. . . . . . 7
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ Β¬ βͺ π¦ = β
) β βͺ π¦
β π« (fiβπ₯)) |
28 | | uni0b 4899 |
. . . . . . . . . 10
β’ (βͺ π¦ =
β
β π¦ β
{β
}) |
29 | 28 | notbii 320 |
. . . . . . . . 9
β’ (Β¬
βͺ π¦ = β
β Β¬ π¦ β {β
}) |
30 | | disjssun 4432 |
. . . . . . . . . . . . 13
β’ ((π¦ β© {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) = β
β (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β π¦ β
{β
})) |
31 | 30 | biimpcd 249 |
. . . . . . . . . . . 12
β’ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
((π¦ β© {π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) = β
β π¦ β
{β
})) |
32 | 31 | necon3bd 2958 |
. . . . . . . . . . 11
β’ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
(Β¬ π¦ β {β
}
β (π¦ β© {π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) β
β
)) |
33 | | n0 4311 |
. . . . . . . . . . . 12
β’ ((π¦ β© {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) β β
β
βπ€ π€ β (π¦ β© {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)})) |
34 | | elin 3931 |
. . . . . . . . . . . . . . 15
β’ (π€ β (π¦ β© {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) β (π€ β π¦ β§ π€ β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)})) |
35 | 8 | anbi2i 624 |
. . . . . . . . . . . . . . 15
β’ ((π€ β π¦ β§ π€ β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) β (π€ β π¦ β§ (π€ β π« (fiβπ₯) β§ (π β π€ β§ βπ β (π« π€ β© Fin) Β¬ π = βͺ π)))) |
36 | 34, 35 | bitri 275 |
. . . . . . . . . . . . . 14
β’ (π€ β (π¦ β© {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) β (π€ β π¦ β§ (π€ β π« (fiβπ₯) β§ (π β π€ β§ βπ β (π« π€ β© Fin) Β¬ π = βͺ π)))) |
37 | | simprrl 780 |
. . . . . . . . . . . . . . 15
β’ ((π€ β π¦ β§ (π€ β π« (fiβπ₯) β§ (π β π€ β§ βπ β (π« π€ β© Fin) Β¬ π = βͺ π))) β π β π€) |
38 | | simpl 484 |
. . . . . . . . . . . . . . 15
β’ ((π€ β π¦ β§ (π€ β π« (fiβπ₯) β§ (π β π€ β§ βπ β (π« π€ β© Fin) Β¬ π = βͺ π))) β π€ β π¦) |
39 | | ssuni 4898 |
. . . . . . . . . . . . . . 15
β’ ((π β π€ β§ π€ β π¦) β π β βͺ π¦) |
40 | 37, 38, 39 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π€ β π¦ β§ (π€ β π« (fiβπ₯) β§ (π β π€ β§ βπ β (π« π€ β© Fin) Β¬ π = βͺ π))) β π β βͺ π¦) |
41 | 36, 40 | sylbi 216 |
. . . . . . . . . . . . 13
β’ (π€ β (π¦ β© {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) β π β βͺ π¦) |
42 | 41 | exlimiv 1934 |
. . . . . . . . . . . 12
β’
(βπ€ π€ β (π¦ β© {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) β π β βͺ π¦) |
43 | 33, 42 | sylbi 216 |
. . . . . . . . . . 11
β’ ((π¦ β© {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) β β
β π β βͺ π¦) |
44 | 32, 43 | syl6 35 |
. . . . . . . . . 10
β’ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
(Β¬ π¦ β {β
}
β π β βͺ π¦)) |
45 | 44 | ad2antrl 727 |
. . . . . . . . 9
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β (Β¬ π¦ β
{β
} β π β
βͺ π¦)) |
46 | 29, 45 | biimtrid 241 |
. . . . . . . 8
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β (Β¬ βͺ π¦ = β
β π β βͺ π¦)) |
47 | 46 | imp 408 |
. . . . . . 7
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ Β¬ βͺ π¦ = β
) β π β βͺ π¦) |
48 | | elfpw 9305 |
. . . . . . . . . 10
β’ (π β (π« βͺ π¦
β© Fin) β (π
β βͺ π¦ β§ π β Fin)) |
49 | | unieq 4881 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = β
β βͺ π¦ =
βͺ β
) |
50 | | uni0 4901 |
. . . . . . . . . . . . . . . . . . 19
β’ βͺ β
= β
|
51 | 49, 50 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = β
β βͺ π¦ =
β
) |
52 | 51 | necon3bi 2971 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
βͺ π¦ = β
β π¦ β β
) |
53 | 52 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((Β¬
βͺ π¦ = β
β§ π β Fin) β π¦ β β
) |
54 | 53 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ ((Β¬ βͺ π¦ = β
β§ π β Fin) β§ π β βͺ π¦)) β π¦ β β
) |
55 | | simplrr 777 |
. . . . . . . . . . . . . . 15
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ ((Β¬ βͺ π¦ = β
β§ π β Fin) β§ π β βͺ π¦)) β [β] Or
π¦) |
56 | | simprlr 779 |
. . . . . . . . . . . . . . 15
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ ((Β¬ βͺ π¦ = β
β§ π β Fin) β§ π β βͺ π¦)) β π β Fin) |
57 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ ((Β¬ βͺ π¦ = β
β§ π β Fin) β§ π β βͺ π¦)) β π β βͺ π¦) |
58 | | finsschain 9310 |
. . . . . . . . . . . . . . 15
β’ (((π¦ β β
β§
[β] Or π¦)
β§ (π β Fin β§
π β βͺ π¦))
β βπ€ β
π¦ π β π€) |
59 | 54, 55, 56, 57, 58 | syl22anc 838 |
. . . . . . . . . . . . . 14
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ ((Β¬ βͺ π¦ = β
β§ π β Fin) β§ π β βͺ π¦)) β βπ€ β π¦ π β π€) |
60 | 59 | expr 458 |
. . . . . . . . . . . . 13
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ (Β¬ βͺ π¦ = β
β§ π β Fin)) β (π β βͺ π¦ β βπ€ β π¦ π β π€)) |
61 | | 0elpw 5316 |
. . . . . . . . . . . . . . . . . . . 20
β’ β
β π« π |
62 | | 0fin 9122 |
. . . . . . . . . . . . . . . . . . . 20
β’ β
β Fin |
63 | 61, 62 | elini 4158 |
. . . . . . . . . . . . . . . . . . 19
β’ β
β (π« π β©
Fin) |
64 | | unieq 4881 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = β
β βͺ π =
βͺ β
) |
65 | 64 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = β
β (π = βͺ
π β π = βͺ
β
)) |
66 | 65 | notbid 318 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = β
β (Β¬ π = βͺ
π β Β¬ π = βͺ
β
)) |
67 | 66 | rspccv 3581 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ β
(π« π β© Fin)
Β¬ π = βͺ π
β (β
β (π« π β© Fin) β Β¬ π = βͺ
β
)) |
68 | 63, 67 | mpi 20 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
(π« π β© Fin)
Β¬ π = βͺ π
β Β¬ π = βͺ β
) |
69 | | velpw 4570 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π« π€ β π β π€) |
70 | | elin 3931 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π« π€ β© Fin) β (π β π« π€ β§ π β Fin)) |
71 | | unieq 4881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = π β βͺ π = βͺ
π) |
72 | 71 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β (π = βͺ π β π = βͺ π)) |
73 | 72 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π β (Β¬ π = βͺ π β Β¬ π = βͺ π)) |
74 | 73 | rspccv 3581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(βπ β
(π« π€ β© Fin)
Β¬ π = βͺ π
β (π β (π«
π€ β© Fin) β Β¬
π = βͺ π)) |
75 | 70, 74 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(βπ β
(π« π€ β© Fin)
Β¬ π = βͺ π
β ((π β π«
π€ β§ π β Fin) β Β¬ π = βͺ π)) |
76 | 75 | expd 417 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(βπ β
(π« π€ β© Fin)
Β¬ π = βͺ π
β (π β π«
π€ β (π β Fin β Β¬ π = βͺ
π))) |
77 | 69, 76 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ β
(π« π€ β© Fin)
Β¬ π = βͺ π
β (π β π€ β (π β Fin β Β¬ π = βͺ π))) |
78 | 77 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(βπ β
(π« π€ β© Fin)
Β¬ π = βͺ π
β (π β Fin β
(π β π€ β Β¬ π = βͺ π))) |
79 | 78 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π€ β π«
(fiβπ₯) β§ (π β π€ β§ βπ β (π« π€ β© Fin) Β¬ π = βͺ π)) β (π β Fin β (π β π€ β Β¬ π = βͺ π))) |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (Β¬
π = βͺ β
β ((π€ β π« (fiβπ₯) β§ (π β π€ β§ βπ β (π« π€ β© Fin) Β¬ π = βͺ π)) β (π β Fin β (π β π€ β Β¬ π = βͺ π)))) |
81 | | sseq2 3975 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π€ = β
β (π β π€ β π β β
)) |
82 | | ss0 4363 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β
β π = β
) |
83 | 81, 82 | syl6bi 253 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π€ = β
β (π β π€ β π = β
)) |
84 | | unieq 4881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = β
β βͺ π =
βͺ β
) |
85 | 84 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = β
β (π = βͺ
π β π = βͺ
β
)) |
86 | 85 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = β
β (Β¬ π = βͺ
π β Β¬ π = βͺ
β
)) |
87 | 86 | biimprcd 250 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (Β¬
π = βͺ β
β (π = β
β Β¬ π = βͺ π)) |
88 | 87 | a1dd 50 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (Β¬
π = βͺ β
β (π = β
β (π β Fin β Β¬ π = βͺ π))) |
89 | 83, 88 | syl9r 78 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Β¬
π = βͺ β
β (π€ = β
β (π β π€ β (π β Fin β Β¬ π = βͺ π)))) |
90 | 89 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (Β¬
π = βͺ β
β (π€ = β
β (π β Fin β (π β π€ β Β¬ π = βͺ π)))) |
91 | 80, 90 | jaod 858 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Β¬
π = βͺ β
β (((π€ β π« (fiβπ₯) β§ (π β π€ β§ βπ β (π« π€ β© Fin) Β¬ π = βͺ π)) β¨ π€ = β
) β (π β Fin β (π β π€ β Β¬ π = βͺ π)))) |
92 | 11, 91 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Β¬
π = βͺ β
β (π€ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
(π β Fin β (π β π€ β Β¬ π = βͺ π)))) |
93 | 1, 92 | sylan9r 510 |
. . . . . . . . . . . . . . . . . . 19
β’ ((Β¬
π = βͺ β
β§ π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})) β
(π€ β π¦ β (π β Fin β (π β π€ β Β¬ π = βͺ π)))) |
94 | 93 | com23 86 |
. . . . . . . . . . . . . . . . . 18
β’ ((Β¬
π = βͺ β
β§ π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})) β
(π β Fin β (π€ β π¦ β (π β π€ β Β¬ π = βͺ π)))) |
95 | 68, 94 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’
((βπ β
(π« π β© Fin)
Β¬ π = βͺ π
β§ π¦ β ({π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})) β
(π β Fin β (π€ β π¦ β (π β π€ β Β¬ π = βͺ π)))) |
96 | 95 | ad2ant2lr 747 |
. . . . . . . . . . . . . . . 16
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β (π β Fin β
(π€ β π¦ β (π β π€ β Β¬ π = βͺ π)))) |
97 | 96 | imp 408 |
. . . . . . . . . . . . . . 15
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ π β Fin) β
(π€ β π¦ β (π β π€ β Β¬ π = βͺ π))) |
98 | 97 | adantrl 715 |
. . . . . . . . . . . . . 14
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ (Β¬ βͺ π¦ = β
β§ π β Fin)) β (π€ β π¦ β (π β π€ β Β¬ π = βͺ π))) |
99 | 98 | rexlimdv 3151 |
. . . . . . . . . . . . 13
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ (Β¬ βͺ π¦ = β
β§ π β Fin)) β (βπ€ β π¦ π β π€ β Β¬ π = βͺ π)) |
100 | 60, 99 | syld 47 |
. . . . . . . . . . . 12
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ (Β¬ βͺ π¦ = β
β§ π β Fin)) β (π β βͺ π¦ β Β¬ π = βͺ π)) |
101 | 100 | expr 458 |
. . . . . . . . . . 11
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ Β¬ βͺ π¦ = β
) β (π β Fin β (π β βͺ π¦ β Β¬ π = βͺ π))) |
102 | 101 | impcomd 413 |
. . . . . . . . . 10
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ Β¬ βͺ π¦ = β
) β ((π β βͺ π¦ β§ π β Fin) β Β¬ π = βͺ π)) |
103 | 48, 102 | biimtrid 241 |
. . . . . . . . 9
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ Β¬ βͺ π¦ = β
) β (π β (π« βͺ π¦
β© Fin) β Β¬ π =
βͺ π)) |
104 | 103 | ralrimiv 3143 |
. . . . . . . 8
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ Β¬ βͺ π¦ = β
) β βπ β (π« βͺ π¦
β© Fin) Β¬ π = βͺ π) |
105 | | unieq 4881 |
. . . . . . . . . . 11
β’ (π = π β βͺ π = βͺ
π) |
106 | 105 | eqeq2d 2748 |
. . . . . . . . . 10
β’ (π = π β (π = βͺ π β π = βͺ π)) |
107 | 106 | notbid 318 |
. . . . . . . . 9
β’ (π = π β (Β¬ π = βͺ π β Β¬ π = βͺ π)) |
108 | 107 | cbvralvw 3228 |
. . . . . . . 8
β’
(βπ β
(π« βͺ π¦ β© Fin) Β¬ π = βͺ π β βπ β (π« βͺ π¦
β© Fin) Β¬ π = βͺ π) |
109 | 104, 108 | sylib 217 |
. . . . . . 7
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ Β¬ βͺ π¦ = β
) β βπ β (π« βͺ π¦
β© Fin) Β¬ π = βͺ π) |
110 | 27, 47, 109 | jca32 517 |
. . . . . 6
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β§ Β¬ βͺ π¦ = β
) β (βͺ π¦
β π« (fiβπ₯) β§ (π β βͺ π¦ β§ βπ β (π« βͺ π¦
β© Fin) Β¬ π = βͺ π))) |
111 | 110 | ex 414 |
. . . . 5
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β (Β¬ βͺ π¦ = β
β (βͺ π¦
β π« (fiβπ₯) β§ (π β βͺ π¦ β§ βπ β (π« βͺ π¦
β© Fin) Β¬ π = βͺ π)))) |
112 | | orcom 869 |
. . . . . 6
β’ ((βͺ π¦
β {β
} β¨ βͺ π¦ β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) β (βͺ π¦
β {π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β¨ βͺ π¦
β {β
})) |
113 | 25 | elsn 4606 |
. . . . . . . 8
β’ (βͺ π¦
β {β
} β βͺ π¦ = β
) |
114 | | sseq2 3975 |
. . . . . . . . . 10
β’ (π§ = βͺ
π¦ β (π β π§ β π β βͺ π¦)) |
115 | | pweq 4579 |
. . . . . . . . . . . 12
β’ (π§ = βͺ
π¦ β π« π§ = π« βͺ π¦) |
116 | 115 | ineq1d 4176 |
. . . . . . . . . . 11
β’ (π§ = βͺ
π¦ β (π« π§ β© Fin) = (π« βͺ π¦
β© Fin)) |
117 | 116 | raleqdv 3316 |
. . . . . . . . . 10
β’ (π§ = βͺ
π¦ β (βπ β (π« π§ β© Fin) Β¬ π = βͺ
π β βπ β (π« βͺ π¦
β© Fin) Β¬ π = βͺ π)) |
118 | 114, 117 | anbi12d 632 |
. . . . . . . . 9
β’ (π§ = βͺ
π¦ β ((π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π) β (π β βͺ π¦ β§ βπ β (π« βͺ π¦
β© Fin) Β¬ π = βͺ π))) |
119 | 118 | elrab 3650 |
. . . . . . . 8
β’ (βͺ π¦
β {π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β (βͺ π¦
β π« (fiβπ₯) β§ (π β βͺ π¦ β§ βπ β (π« βͺ π¦
β© Fin) Β¬ π = βͺ π))) |
120 | 113, 119 | orbi12i 914 |
. . . . . . 7
β’ ((βͺ π¦
β {β
} β¨ βͺ π¦ β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) β (βͺ π¦ =
β
β¨ (βͺ π¦ β π« (fiβπ₯) β§ (π β βͺ π¦ β§ βπ β (π« βͺ π¦
β© Fin) Β¬ π = βͺ π)))) |
121 | | df-or 847 |
. . . . . . 7
β’ ((βͺ π¦ =
β
β¨ (βͺ π¦ β π« (fiβπ₯) β§ (π β βͺ π¦ β§ βπ β (π« βͺ π¦
β© Fin) Β¬ π = βͺ π)))
β (Β¬ βͺ π¦ = β
β (βͺ π¦
β π« (fiβπ₯) β§ (π β βͺ π¦ β§ βπ β (π« βͺ π¦
β© Fin) Β¬ π = βͺ π)))) |
122 | 120, 121 | bitr2i 276 |
. . . . . 6
β’ ((Β¬
βͺ π¦ = β
β (βͺ π¦
β π« (fiβπ₯) β§ (π β βͺ π¦ β§ βπ β (π« βͺ π¦
β© Fin) Β¬ π = βͺ π)))
β (βͺ π¦ β {β
} β¨ βͺ π¦
β {π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)})) |
123 | | elun 4113 |
. . . . . 6
β’ (βͺ π¦
β ({π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
(βͺ π¦ β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β¨ βͺ π¦
β {β
})) |
124 | 112, 122,
123 | 3bitr4i 303 |
. . . . 5
β’ ((Β¬
βͺ π¦ = β
β (βͺ π¦
β π« (fiβπ₯) β§ (π β βͺ π¦ β§ βπ β (π« βͺ π¦
β© Fin) Β¬ π = βͺ π)))
β βͺ π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ
{β
})) |
125 | 111, 124 | sylib 217 |
. . . 4
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ (π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦))
β βͺ π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ
{β
})) |
126 | 125 | ex 414 |
. . 3
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β ((π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦)
β βͺ π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ
{β
}))) |
127 | 126 | alrimiv 1931 |
. 2
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β βπ¦((π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦)
β βͺ π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ
{β
}))) |
128 | | fvex 6860 |
. . . . . 6
β’
(fiβπ₯) β
V |
129 | 128 | pwex 5340 |
. . . . 5
β’ π«
(fiβπ₯) β
V |
130 | 129 | rabex 5294 |
. . . 4
β’ {π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β V |
131 | | p0ex 5344 |
. . . 4
β’ {β
}
β V |
132 | 130, 131 | unex 7685 |
. . 3
β’ ({π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
V |
133 | 132 | zorn 10450 |
. 2
β’
(βπ¦((π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§
[β] Or π¦)
β βͺ π¦ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})) β
βπ’ β ({π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£) |
134 | 127, 133 | syl 17 |
1
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β βπ’ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£) |