Step | Hyp | Ref
| Expression |
1 | | ralnex 3076 |
. . . . 5
β’
(βπ β
(π« π β© Fin)
Β¬ π = βͺ π
β Β¬ βπ
β (π« π β©
Fin)π = βͺ π) |
2 | | alexsubALT.1 |
. . . . . . . 8
β’ π = βͺ
π½ |
3 | 2 | alexsubALTlem2 23415 |
. . . . . . 7
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β βπ’ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£) |
4 | | elun 4113 |
. . . . . . . . . 10
β’ (π’ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
(π’ β {π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β¨ π’ β {β
})) |
5 | | sseq2 3975 |
. . . . . . . . . . . . 13
β’ (π§ = π’ β (π β π§ β π β π’)) |
6 | | pweq 4579 |
. . . . . . . . . . . . . . 15
β’ (π§ = π’ β π« π§ = π« π’) |
7 | 6 | ineq1d 4176 |
. . . . . . . . . . . . . 14
β’ (π§ = π’ β (π« π§ β© Fin) = (π« π’ β© Fin)) |
8 | 7 | raleqdv 3316 |
. . . . . . . . . . . . 13
β’ (π§ = π’ β (βπ β (π« π§ β© Fin) Β¬ π = βͺ π β βπ β (π« π’ β© Fin) Β¬ π = βͺ
π)) |
9 | 5, 8 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π§ = π’ β ((π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π) β (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) |
10 | 9 | elrab 3650 |
. . . . . . . . . . 11
β’ (π’ β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) |
11 | | velsn 4607 |
. . . . . . . . . . 11
β’ (π’ β {β
} β π’ = β
) |
12 | 10, 11 | orbi12i 914 |
. . . . . . . . . 10
β’ ((π’ β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β¨ π’ β {β
}) β ((π’ β π«
(fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) β¨ π’ = β
)) |
13 | 4, 12 | bitri 275 |
. . . . . . . . 9
β’ (π’ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
((π’ β π«
(fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) β¨ π’ = β
)) |
14 | | ralnex 3076 |
. . . . . . . . . . . . 13
β’
(βπ£ β
({π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£) |
15 | | simprrl 780 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β π β π’) |
16 | 15 | unissd 4880 |
. . . . . . . . . . . . . . . 16
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β βͺ π
β βͺ π’) |
17 | | sseq1 3974 |
. . . . . . . . . . . . . . . 16
β’ (π = βͺ
π β (π β βͺ π’ β βͺ π
β βͺ π’)) |
18 | 16, 17 | syl5ibrcom 247 |
. . . . . . . . . . . . . . 15
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (π = βͺ π β π β βͺ π’)) |
19 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ π₯ β V |
20 | | inss1 4193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π₯ β© π’) β π₯ |
21 | 19, 20 | elpwi2 5308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π₯ β© π’) β π« π₯ |
22 | | unieq 4881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = (π₯ β© π’) β βͺ π = βͺ
(π₯ β© π’)) |
23 | 22 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = (π₯ β© π’) β (π = βͺ π β π = βͺ (π₯ β© π’))) |
24 | | pweq 4579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = (π₯ β© π’) β π« π = π« (π₯ β© π’)) |
25 | 24 | ineq1d 4176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = (π₯ β© π’) β (π« π β© Fin) = (π« (π₯ β© π’) β© Fin)) |
26 | 25 | rexeqdv 3317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = (π₯ β© π’) β (βπ β (π« π β© Fin)π = βͺ π β βπ β (π« (π₯ β© π’) β© Fin)π = βͺ π)) |
27 | 23, 26 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = (π₯ β© π’) β ((π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β (π = βͺ (π₯ β© π’) β βπ β (π« (π₯ β© π’) β© Fin)π = βͺ π))) |
28 | 27 | rspccv 3581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β ((π₯ β© π’) β π« π₯ β (π = βͺ (π₯ β© π’) β βπ β (π« (π₯ β© π’) β© Fin)π = βͺ π))) |
29 | 21, 28 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (π = βͺ (π₯ β© π’) β βπ β (π« (π₯ β© π’) β© Fin)π = βͺ π)) |
30 | | inss2 4194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π₯ β© π’) β π’ |
31 | | sstr 3957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β (π₯ β© π’) β§ (π₯ β© π’) β π’) β π β π’) |
32 | 30, 31 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (π₯ β© π’) β π β π’) |
33 | 32 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β (π₯ β© π’) β§ π β Fin) β (π β π’ β§ π β Fin)) |
34 | | elfpw 9305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (π« (π₯ β© π’) β© Fin) β (π β (π₯ β© π’) β§ π β Fin)) |
35 | | elfpw 9305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (π« π’ β© Fin) β (π β π’ β§ π β Fin)) |
36 | 33, 34, 35 | 3imtr4i 292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π« (π₯ β© π’) β© Fin) β π β (π« π’ β© Fin)) |
37 | 36 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β (π« (π₯ β© π’) β© Fin) β§ π = βͺ π) β (π β (π« π’ β© Fin) β§ π = βͺ π)) |
38 | 37 | reximi2 3083 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(βπ β
(π« (π₯ β© π’) β© Fin)π = βͺ π β βπ β (π« π’ β© Fin)π = βͺ π) |
39 | 29, 38 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (π = βͺ (π₯ β© π’) β βπ β (π« π’ β© Fin)π = βͺ π)) |
40 | | unieq 4881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π β βͺ π = βͺ
π) |
41 | 40 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = π β (π = βͺ π β π = βͺ π)) |
42 | 41 | cbvrexvw 3229 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ β
(π« π’ β©
Fin)π = βͺ π
β βπ β
(π« π’ β©
Fin)π = βͺ π) |
43 | 39, 42 | syl6ib 251 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (π = βͺ (π₯ β© π’) β βπ β (π« π’ β© Fin)π = βͺ π)) |
44 | | dfrex2 3077 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(βπ β
(π« π’ β©
Fin)π = βͺ π
β Β¬ βπ
β (π« π’ β©
Fin) Β¬ π = βͺ π) |
45 | 43, 44 | syl6ib 251 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (π = βͺ (π₯ β© π’) β Β¬ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) |
46 | 45 | con2d 134 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (βπ β (π« π’ β© Fin) Β¬ π = βͺ
π β Β¬ π = βͺ
(π₯ β© π’))) |
47 | 46 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (π β π’ β (βπ β (π« π’ β© Fin) Β¬ π = βͺ π β Β¬ π = βͺ (π₯ β© π’)))) |
48 | 47 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β (π β π’ β (βπ β (π« π’ β© Fin) Β¬ π = βͺ π β Β¬ π = βͺ (π₯ β© π’)))) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ π’ β π« (fiβπ₯)) β (π β π’ β (βπ β (π« π’ β© Fin) Β¬ π = βͺ π β Β¬ π = βͺ (π₯ β© π’)))) |
50 | 49 | impd 412 |
. . . . . . . . . . . . . . . . . 18
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ π’ β π« (fiβπ₯)) β ((π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π) β Β¬ π = βͺ (π₯ β© π’))) |
51 | 50 | impr 456 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β Β¬ π = βͺ
(π₯ β© π’)) |
52 | 20 | unissi 4879 |
. . . . . . . . . . . . . . . . . . 19
β’ βͺ (π₯
β© π’) β βͺ π₯ |
53 | | fiuni 9371 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ β V β βͺ π₯ =
βͺ (fiβπ₯)) |
54 | 53 | elv 3454 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ βͺ π₯ =
βͺ (fiβπ₯) |
55 | | fibas 22343 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(fiβπ₯) β
TopBases |
56 | | unitg 22333 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((fiβπ₯) β
TopBases β βͺ (topGenβ(fiβπ₯)) = βͺ (fiβπ₯)) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ βͺ (topGenβ(fiβπ₯)) = βͺ
(fiβπ₯) |
58 | 54, 57 | eqtr4i 2768 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ βͺ π₯ =
βͺ (topGenβ(fiβπ₯)) |
59 | | unieq 4881 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π½ = (topGenβ(fiβπ₯)) β βͺ π½ =
βͺ (topGenβ(fiβπ₯))) |
60 | 58, 59 | eqtr4id 2796 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π½ = (topGenβ(fiβπ₯)) β βͺ π₯ =
βͺ π½) |
61 | 60, 2 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π½ = (topGenβ(fiβπ₯)) β βͺ π₯ =
π) |
62 | 61 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β βͺ π₯ =
π) |
63 | 62 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β βͺ π₯ =
π) |
64 | 52, 63 | sseqtrid 4001 |
. . . . . . . . . . . . . . . . . 18
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β βͺ (π₯
β© π’) β π) |
65 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = βͺ
(π₯ β© π’) β βͺ (π₯ β© π’) = π) |
66 | | eqss 3964 |
. . . . . . . . . . . . . . . . . . . 20
β’ (βͺ (π₯
β© π’) = π β (βͺ (π₯
β© π’) β π β§ π β βͺ (π₯ β© π’))) |
67 | 66 | baib 537 |
. . . . . . . . . . . . . . . . . . 19
β’ (βͺ (π₯
β© π’) β π β (βͺ (π₯
β© π’) = π β π β βͺ (π₯ β© π’))) |
68 | 65, 67 | bitrid 283 |
. . . . . . . . . . . . . . . . . 18
β’ (βͺ (π₯
β© π’) β π β (π = βͺ (π₯ β© π’) β π β βͺ (π₯ β© π’))) |
69 | 64, 68 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (π = βͺ (π₯ β© π’) β π β βͺ (π₯ β© π’))) |
70 | 51, 69 | mtbid 324 |
. . . . . . . . . . . . . . . 16
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β Β¬ π β βͺ (π₯
β© π’)) |
71 | | sstr2 3956 |
. . . . . . . . . . . . . . . . 17
β’ (π β βͺ π’
β (βͺ π’ β βͺ (π₯ β© π’) β π β βͺ (π₯ β© π’))) |
72 | 71 | con3rr3 155 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π β βͺ (π₯
β© π’) β (π β βͺ π’
β Β¬ βͺ π’ β βͺ (π₯ β© π’))) |
73 | 70, 72 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (π β βͺ π’ β Β¬ βͺ π’
β βͺ (π₯ β© π’))) |
74 | | nss 4011 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
βͺ π’ β βͺ (π₯ β© π’) β βπ¦(π¦ β βͺ π’ β§ Β¬ π¦ β βͺ (π₯ β© π’))) |
75 | | df-rex 3075 |
. . . . . . . . . . . . . . . . 17
β’
(βπ¦ β
βͺ π’ Β¬ π¦ β βͺ (π₯ β© π’) β βπ¦(π¦ β βͺ π’ β§ Β¬ π¦ β βͺ (π₯ β© π’))) |
76 | 74, 75 | bitr4i 278 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
βͺ π’ β βͺ (π₯ β© π’) β βπ¦ β βͺ π’ Β¬ π¦ β βͺ (π₯ β© π’)) |
77 | | eluni2 4874 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β βͺ π’
β βπ€ β
π’ π¦ β π€) |
78 | | elpwi 4572 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π’ β π«
(fiβπ₯) β π’ β (fiβπ₯)) |
79 | 78 | sseld 3948 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π’ β π«
(fiβπ₯) β (π€ β π’ β π€ β (fiβπ₯))) |
80 | 79 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (π€ β π’ β π€ β (fiβπ₯))) |
81 | | elfi 9356 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π€ β V β§ π₯ β V) β (π€ β (fiβπ₯) β βπ‘ β (π« π₯ β© Fin)π€ = β© π‘)) |
82 | 81 | el2v 3456 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β (fiβπ₯) β βπ‘ β (π« π₯ β© Fin)π€ = β© π‘) |
83 | 80, 82 | syl6ib 251 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (π€ β π’ β βπ‘ β (π« π₯ β© Fin)π€ = β© π‘)) |
84 | 2 | alexsubALTlem3 23416 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β βπ β π‘ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π) |
85 | 78 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π’ β π«
(fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) β π’ β (fiβπ₯)) |
86 | 85 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π’ β (fiβπ₯)) |
87 | | ssfii 9362 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π₯ β V β π₯ β (fiβπ₯)) |
88 | 87 | elv 3454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ π₯ β (fiβπ₯) |
89 | | elinel1 4160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π‘ β (π« π₯ β© Fin) β π‘ β π« π₯) |
90 | 89 | elpwid 4574 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π‘ β (π« π₯ β© Fin) β π‘ β π₯) |
91 | 90 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π‘ β (π« π₯ β© Fin) β§ π€ = β©
π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’))) β π‘ β π₯) |
92 | 91 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π‘ β π₯) |
93 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π β π‘) |
94 | 92, 93 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π β π₯) |
95 | 88, 94 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π β (fiβπ₯)) |
96 | 95 | snssd 4774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β {π } β (fiβπ₯)) |
97 | 86, 96 | unssd 4151 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β (π’ βͺ {π }) β (fiβπ₯)) |
98 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(fiβπ₯) β
V |
99 | 98 | elpw2 5307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π’ βͺ {π }) β π« (fiβπ₯) β (π’ βͺ {π }) β (fiβπ₯)) |
100 | 97, 99 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β (π’ βͺ {π }) β π« (fiβπ₯)) |
101 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π’ β π«
(fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) β π β π’) |
102 | 101 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π β π’) |
103 | | ssun1 4137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ π’ β (π’ βͺ {π }) |
104 | 102, 103 | sstrdi 3961 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π β (π’ βͺ {π })) |
105 | | unieq 4881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = π β βͺ π = βͺ
π) |
106 | 105 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = π β (π = βͺ π β π = βͺ π)) |
107 | 106 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = π β (Β¬ π = βͺ π β Β¬ π = βͺ π)) |
108 | 107 | cbvralvw 3228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(βπ β
(π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ
π β βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π) |
109 | 108 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(βπ β
(π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ
π β βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π) |
110 | 109 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π) |
111 | 100, 104,
110 | jca32 517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β ((π’ βͺ {π }) β π« (fiβπ₯) β§ (π β (π’ βͺ {π }) β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) |
112 | | sseq2 3975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π§ = (π’ βͺ {π }) β (π β π§ β π β (π’ βͺ {π }))) |
113 | | pweq 4579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π§ = (π’ βͺ {π }) β π« π§ = π« (π’ βͺ {π })) |
114 | 113 | ineq1d 4176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π§ = (π’ βͺ {π }) β (π« π§ β© Fin) = (π« (π’ βͺ {π }) β© Fin)) |
115 | 114 | raleqdv 3316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π§ = (π’ βͺ {π }) β (βπ β (π« π§ β© Fin) Β¬ π = βͺ π β βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) |
116 | 112, 115 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π§ = (π’ βͺ {π }) β ((π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π) β (π β (π’ βͺ {π }) β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) |
117 | 116 | elrab 3650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π’ βͺ {π }) β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β ((π’ βͺ {π }) β π« (fiβπ₯) β§ (π β (π’ βͺ {π }) β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) |
118 | 111, 117 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β (π’ βͺ {π }) β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) |
119 | | elun1 4141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π’ βͺ {π }) β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β (π’ βͺ {π }) β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ
{β
})) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β (π’ βͺ {π }) β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ
{β
})) |
121 | | vsnid 4628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ π β {π } |
122 | | elun2 4142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β {π } β π β (π’ βͺ {π })) |
123 | 121, 122 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ π β (π’ βͺ {π }) |
124 | | intss1 4929 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (π β π‘ β β© π‘ β π ) |
125 | | sseq1 3974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (π€ = β©
π‘ β (π€ β π β β© π‘ β π )) |
126 | 124, 125 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (π β π‘ β (π€ = β© π‘ β π€ β π )) |
127 | 126 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π€ = β©
π‘ β§ π β π‘) β π€ β π ) |
128 | 127 | ad4ant24 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((((π‘ β (π« π₯ β© Fin) β§ π€ = β©
π‘) β§ π¦ β π€) β§ π β π‘) β π€ β π ) |
129 | 128 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π€ β π’ β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ π β π‘)) β π€ β π ) |
130 | 129 | adantrrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π€ β π’ β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β π€ β π ) |
131 | 130 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β π€ β π ) |
132 | | simprlr 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β π¦ β π€) |
133 | 131, 132 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β π¦ β π ) |
134 | 90 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (((π‘ β (π« π₯ β© Fin) β§ π€ = β©
π‘) β§ π¦ β π€) β π‘ β π₯) |
135 | 134 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β π‘ β π₯) |
136 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β π β π‘) |
137 | 135, 136 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β π β π₯) |
138 | | elin 3931 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β (π₯ β© π’) β (π β π₯ β§ π β π’)) |
139 | | elunii 4875 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π¦ β π β§ π β (π₯ β© π’)) β π¦ β βͺ (π₯ β© π’)) |
140 | 139 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π¦ β π β (π β (π₯ β© π’) β π¦ β βͺ (π₯ β© π’))) |
141 | 138, 140 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π¦ β π β ((π β π₯ β§ π β π’) β π¦ β βͺ (π₯ β© π’))) |
142 | 141 | expd 417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π¦ β π β (π β π₯ β (π β π’ β π¦ β βͺ (π₯ β© π’)))) |
143 | 133, 137,
142 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β (π β π’ β π¦ β βͺ (π₯ β© π’))) |
144 | 143 | con3d 152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β (Β¬ π¦ β βͺ (π₯
β© π’) β Β¬ π β π’)) |
145 | 144 | expr 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€)) β ((π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π) β (Β¬ π¦ β βͺ (π₯
β© π’) β Β¬ π β π’))) |
146 | 145 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€)) β (Β¬ π¦ β βͺ (π₯ β© π’) β ((π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π) β Β¬ π β π’))) |
147 | 146 | exp32 422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β (π¦ β π€ β (Β¬ π¦ β βͺ (π₯ β© π’) β ((π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π) β Β¬ π β π’))))) |
148 | 147 | imp55 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β Β¬ π β π’) |
149 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ π β V |
150 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π£ = π β (π£ β (π’ βͺ {π }) β π β (π’ βͺ {π }))) |
151 | | elequ1 2114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π£ = π β (π£ β π’ β π β π’)) |
152 | 151 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π£ = π β (Β¬ π£ β π’ β Β¬ π β π’)) |
153 | 150, 152 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π£ = π β ((π£ β (π’ βͺ {π }) β§ Β¬ π£ β π’) β (π β (π’ βͺ {π }) β§ Β¬ π β π’))) |
154 | 149, 153 | spcev 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β (π’ βͺ {π }) β§ Β¬ π β π’) β βπ£(π£ β (π’ βͺ {π }) β§ Β¬ π£ β π’)) |
155 | 123, 148,
154 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β βπ£(π£ β (π’ βͺ {π }) β§ Β¬ π£ β π’)) |
156 | | nss 4011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (Β¬
(π’ βͺ {π }) β π’ β βπ£(π£ β (π’ βͺ {π }) β§ Β¬ π£ β π’)) |
157 | 155, 156 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β Β¬ (π’ βͺ {π }) β π’) |
158 | | eqimss2 4006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π’ = (π’ βͺ {π }) β (π’ βͺ {π }) β π’) |
159 | 158 | necon3bi 2971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (Β¬
(π’ βͺ {π }) β π’ β π’ β (π’ βͺ {π })) |
160 | 157, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π’ β (π’ βͺ {π })) |
161 | 160, 103 | jctil 521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β (π’ β (π’ βͺ {π }) β§ π’ β (π’ βͺ {π }))) |
162 | | df-pss 3934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π’ β (π’ βͺ {π }) β (π’ β (π’ βͺ {π }) β§ π’ β (π’ βͺ {π }))) |
163 | 161, 162 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π’ β (π’ βͺ {π })) |
164 | | psseq2 4053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π£ = (π’ βͺ {π }) β (π’ β π£ β π’ β (π’ βͺ {π }))) |
165 | 164 | rspcev 3584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π’ βͺ {π }) β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§ π’ β (π’ βͺ {π })) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£) |
166 | 120, 163,
165 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£) |
167 | 84, 166 | rexlimddv 3159 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£) |
168 | 167 | exp45 440 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β (π¦ β π€ β (Β¬ π¦ β βͺ (π₯ β© π’) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£)))) |
169 | 168 | expd 417 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β (π‘ β (π« π₯ β© Fin) β (π€ = β© π‘ β (π¦ β π€ β (Β¬ π¦ β βͺ (π₯ β© π’) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£))))) |
170 | 169 | rexlimdv 3151 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β (βπ‘ β (π« π₯ β© Fin)π€ = β© π‘ β (π¦ β π€ β (Β¬ π¦ β βͺ (π₯ β© π’) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£)))) |
171 | 170 | ex 414 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (π€ β π’ β (βπ‘ β (π« π₯ β© Fin)π€ = β© π‘ β (π¦ β π€ β (Β¬ π¦ β βͺ (π₯ β© π’) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£))))) |
172 | 83, 171 | mpdd 43 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (π€ β π’ β (π¦ β π€ β (Β¬ π¦ β βͺ (π₯ β© π’) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£)))) |
173 | 172 | rexlimdv 3151 |
. . . . . . . . . . . . . . . . . 18
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (βπ€ β π’ π¦ β π€ β (Β¬ π¦ β βͺ (π₯ β© π’) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£))) |
174 | 77, 173 | biimtrid 241 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (π¦ β βͺ π’ β (Β¬ π¦ β βͺ (π₯
β© π’) β
βπ£ β ({π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£))) |
175 | 174 | rexlimdv 3151 |
. . . . . . . . . . . . . . . 16
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (βπ¦ β βͺ π’
Β¬ π¦ β βͺ (π₯
β© π’) β
βπ£ β ({π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£)) |
176 | 76, 175 | biimtrid 241 |
. . . . . . . . . . . . . . 15
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (Β¬ βͺ π’
β βͺ (π₯ β© π’) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£)) |
177 | 18, 73, 176 | 3syld 60 |
. . . . . . . . . . . . . 14
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (π = βͺ π β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£)) |
178 | 177 | con3d 152 |
. . . . . . . . . . . . 13
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (Β¬ βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£ β Β¬ π = βͺ π)) |
179 | 14, 178 | biimtrid 241 |
. . . . . . . . . . . 12
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π = βͺ π)) |
180 | 179 | ex 414 |
. . . . . . . . . . 11
β’ ((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β ((π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) β (βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π = βͺ π))) |
181 | 180 | adantr 482 |
. . . . . . . . . 10
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β ((π’ β π«
(fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) β (βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π = βͺ π))) |
182 | | ssun1 4137 |
. . . . . . . . . . . . . 14
β’ {π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ
{β
}) |
183 | | eqimss2 4006 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π β π β π§) |
184 | 183 | biantrurd 534 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β (βπ β (π« π§ β© Fin) Β¬ π = βͺ π β (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π))) |
185 | | pweq 4579 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = π β π« π§ = π« π) |
186 | 185 | ineq1d 4176 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π β (π« π§ β© Fin) = (π« π β© Fin)) |
187 | 186 | raleqdv 3316 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β (βπ β (π« π§ β© Fin) Β¬ π = βͺ π β βπ β (π« π β© Fin) Β¬ π = βͺ
π)) |
188 | 184, 187 | bitr3d 281 |
. . . . . . . . . . . . . . 15
β’ (π§ = π β ((π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π) β βπ β (π« π β© Fin) Β¬ π = βͺ
π)) |
189 | | simpll3 1215 |
. . . . . . . . . . . . . . 15
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β π β π« (fiβπ₯)) |
190 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β βπ β (π« π β© Fin) Β¬ π = βͺ π) |
191 | 188, 189,
190 | elrabd 3652 |
. . . . . . . . . . . . . 14
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β π β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) |
192 | 182, 191 | sselid 3947 |
. . . . . . . . . . . . 13
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β π β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ
{β
})) |
193 | | psseq2 4053 |
. . . . . . . . . . . . . . 15
β’ (π£ = π β (π’ β π£ β π’ β π)) |
194 | 193 | notbid 318 |
. . . . . . . . . . . . . 14
β’ (π£ = π β (Β¬ π’ β π£ β Β¬ π’ β π)) |
195 | 194 | rspcv 3580 |
. . . . . . . . . . . . 13
β’ (π β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
(βπ£ β ({π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π’ β π)) |
196 | 192, 195 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β (βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π’ β π)) |
197 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π = β
β π = β
) |
198 | | 0elpw 5316 |
. . . . . . . . . . . . . . . . . 18
β’ β
β π« π |
199 | | 0fin 9122 |
. . . . . . . . . . . . . . . . . 18
β’ β
β Fin |
200 | 198, 199 | elini 4158 |
. . . . . . . . . . . . . . . . 17
β’ β
β (π« π β©
Fin) |
201 | 197, 200 | eqeltrdi 2846 |
. . . . . . . . . . . . . . . 16
β’ (π = β
β π β (π« π β© Fin)) |
202 | | unieq 4881 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β βͺ π = βͺ
π) |
203 | 202 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π = βͺ π β π = βͺ π)) |
204 | 203 | notbid 318 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (Β¬ π = βͺ π β Β¬ π = βͺ π)) |
205 | 204 | rspccv 3581 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
(π« π β© Fin)
Β¬ π = βͺ π
β (π β (π«
π β© Fin) β Β¬
π = βͺ π)) |
206 | 201, 205 | syl5 34 |
. . . . . . . . . . . . . . 15
β’
(βπ β
(π« π β© Fin)
Β¬ π = βͺ π
β (π = β
β
Β¬ π = βͺ π)) |
207 | 206 | necon2ad 2959 |
. . . . . . . . . . . . . 14
β’
(βπ β
(π« π β© Fin)
Β¬ π = βͺ π
β (π = βͺ π
β π β
β
)) |
208 | 207 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β (π = βͺ π β π β β
)) |
209 | | psseq1 4052 |
. . . . . . . . . . . . . . 15
β’ (π’ = β
β (π’ β π β β
β π)) |
210 | 209 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β (π’ β π β β
β π)) |
211 | | 0pss 4409 |
. . . . . . . . . . . . . 14
β’ (β
β π β π β β
) |
212 | 210, 211 | bitrdi 287 |
. . . . . . . . . . . . 13
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β (π’ β π β π β β
)) |
213 | 208, 212 | sylibrd 259 |
. . . . . . . . . . . 12
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β (π = βͺ π β π’ β π)) |
214 | 196, 213 | nsyld 156 |
. . . . . . . . . . 11
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β (βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π = βͺ π)) |
215 | 214 | ex 414 |
. . . . . . . . . 10
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β (π’ = β
β (βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π = βͺ π))) |
216 | 181, 215 | jaod 858 |
. . . . . . . . 9
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β (((π’ β π«
(fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) β¨ π’ = β
) β (βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π = βͺ π))) |
217 | 13, 216 | biimtrid 241 |
. . . . . . . 8
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β (π’ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
(βπ£ β ({π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π = βͺ π))) |
218 | 217 | rexlimdv 3151 |
. . . . . . 7
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β (βπ’ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π = βͺ π)) |
219 | 3, 218 | mpd 15 |
. . . . . 6
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β Β¬ π = βͺ
π) |
220 | 219 | ex 414 |
. . . . 5
β’ ((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β (βπ β (π« π β© Fin) Β¬ π = βͺ
π β Β¬ π = βͺ
π)) |
221 | 1, 220 | biimtrrid 242 |
. . . 4
β’ ((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β (Β¬ βπ β (π« π β© Fin)π = βͺ π β Β¬ π = βͺ π)) |
222 | 221 | con4d 115 |
. . 3
β’ ((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)) |
223 | 222 | 3exp 1120 |
. 2
β’ (π½ = (topGenβ(fiβπ₯)) β (βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β (π β π« (fiβπ₯) β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)))) |
224 | 223 | ralrimdv 3150 |
1
β’ (π½ = (topGenβ(fiβπ₯)) β (βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β βπ β π«
(fiβπ₯)(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π))) |