| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ralnex 3071 |
. . . . 5
β’
(βπ β
(π« π β© Fin)
Β¬ π = βͺ π
β Β¬ βπ
β (π« π β©
Fin)π = βͺ π) |
| 2 | | alexsubALT.1 |
. . . . . . . 8
β’ π = βͺ
π½ |
| 3 | 2 | alexsubALTlem2 23773 |
. . . . . . 7
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β βπ’ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£) |
| 4 | | elun 4148 |
. . . . . . . . . 10
β’ (π’ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
(π’ β {π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β¨ π’ β {β
})) |
| 5 | | sseq2 4008 |
. . . . . . . . . . . . 13
β’ (π§ = π’ β (π β π§ β π β π’)) |
| 6 | | pweq 4616 |
. . . . . . . . . . . . . . 15
β’ (π§ = π’ β π« π§ = π« π’) |
| 7 | 6 | ineq1d 4211 |
. . . . . . . . . . . . . 14
β’ (π§ = π’ β (π« π§ β© Fin) = (π« π’ β© Fin)) |
| 8 | 7 | raleqdv 3324 |
. . . . . . . . . . . . 13
β’ (π§ = π’ β (βπ β (π« π§ β© Fin) Β¬ π = βͺ π β βπ β (π« π’ β© Fin) Β¬ π = βͺ
π)) |
| 9 | 5, 8 | anbi12d 630 |
. . . . . . . . . . . 12
β’ (π§ = π’ β ((π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π) β (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) |
| 10 | 9 | elrab 3683 |
. . . . . . . . . . 11
β’ (π’ β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) |
| 11 | | velsn 4644 |
. . . . . . . . . . 11
β’ (π’ β {β
} β π’ = β
) |
| 12 | 10, 11 | orbi12i 912 |
. . . . . . . . . 10
β’ ((π’ β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β¨ π’ β {β
}) β ((π’ β π«
(fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) β¨ π’ = β
)) |
| 13 | 4, 12 | bitri 275 |
. . . . . . . . 9
β’ (π’ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
((π’ β π«
(fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) β¨ π’ = β
)) |
| 14 | | ralnex 3071 |
. . . . . . . . . . . . 13
β’
(βπ£ β
({π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£) |
| 15 | | simprrl 778 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β π β π’) |
| 16 | 15 | unissd 4918 |
. . . . . . . . . . . . . . . 16
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β βͺ π
β βͺ π’) |
| 17 | | sseq1 4007 |
. . . . . . . . . . . . . . . 16
β’ (π = βͺ
π β (π β βͺ π’ β βͺ π
β βͺ π’)) |
| 18 | 16, 17 | syl5ibrcom 246 |
. . . . . . . . . . . . . . 15
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (π = βͺ π β π β βͺ π’)) |
| 19 | | vex 3477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ π₯ β V |
| 20 | | inss1 4228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π₯ β© π’) β π₯ |
| 21 | 19, 20 | elpwi2 5346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π₯ β© π’) β π« π₯ |
| 22 | | unieq 4919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = (π₯ β© π’) β βͺ π = βͺ
(π₯ β© π’)) |
| 23 | 22 | eqeq2d 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = (π₯ β© π’) β (π = βͺ π β π = βͺ (π₯ β© π’))) |
| 24 | | pweq 4616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = (π₯ β© π’) β π« π = π« (π₯ β© π’)) |
| 25 | 24 | ineq1d 4211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = (π₯ β© π’) β (π« π β© Fin) = (π« (π₯ β© π’) β© Fin)) |
| 26 | 25 | rexeqdv 3325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = (π₯ β© π’) β (βπ β (π« π β© Fin)π = βͺ π β βπ β (π« (π₯ β© π’) β© Fin)π = βͺ π)) |
| 27 | 23, 26 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = (π₯ β© π’) β ((π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β (π = βͺ (π₯ β© π’) β βπ β (π« (π₯ β© π’) β© Fin)π = βͺ π))) |
| 28 | 27 | rspccv 3609 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β ((π₯ β© π’) β π« π₯ β (π = βͺ (π₯ β© π’) β βπ β (π« (π₯ β© π’) β© Fin)π = βͺ π))) |
| 29 | 21, 28 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (π = βͺ (π₯ β© π’) β βπ β (π« (π₯ β© π’) β© Fin)π = βͺ π)) |
| 30 | | inss2 4229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π₯ β© π’) β π’ |
| 31 | | sstr 3990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β (π₯ β© π’) β§ (π₯ β© π’) β π’) β π β π’) |
| 32 | 30, 31 | mpan2 688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (π₯ β© π’) β π β π’) |
| 33 | 32 | anim1i 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β (π₯ β© π’) β§ π β Fin) β (π β π’ β§ π β Fin)) |
| 34 | | elfpw 9358 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (π« (π₯ β© π’) β© Fin) β (π β (π₯ β© π’) β§ π β Fin)) |
| 35 | | elfpw 9358 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (π« π’ β© Fin) β (π β π’ β§ π β Fin)) |
| 36 | 33, 34, 35 | 3imtr4i 292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π« (π₯ β© π’) β© Fin) β π β (π« π’ β© Fin)) |
| 37 | 36 | anim1i 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β (π« (π₯ β© π’) β© Fin) β§ π = βͺ π) β (π β (π« π’ β© Fin) β§ π = βͺ π)) |
| 38 | 37 | reximi2 3078 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(βπ β
(π« (π₯ β© π’) β© Fin)π = βͺ π β βπ β (π« π’ β© Fin)π = βͺ π) |
| 39 | 29, 38 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (π = βͺ (π₯ β© π’) β βπ β (π« π’ β© Fin)π = βͺ π)) |
| 40 | | unieq 4919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π β βͺ π = βͺ
π) |
| 41 | 40 | eqeq2d 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = π β (π = βͺ π β π = βͺ π)) |
| 42 | 41 | cbvrexvw 3234 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ β
(π« π’ β©
Fin)π = βͺ π
β βπ β
(π« π’ β©
Fin)π = βͺ π) |
| 43 | 39, 42 | imbitrdi 250 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (π = βͺ (π₯ β© π’) β βπ β (π« π’ β© Fin)π = βͺ π)) |
| 44 | | dfrex2 3072 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(βπ β
(π« π’ β©
Fin)π = βͺ π
β Β¬ βπ
β (π« π’ β©
Fin) Β¬ π = βͺ π) |
| 45 | 43, 44 | imbitrdi 250 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (π = βͺ (π₯ β© π’) β Β¬ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) |
| 46 | 45 | con2d 134 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (βπ β (π« π’ β© Fin) Β¬ π = βͺ
π β Β¬ π = βͺ
(π₯ β© π’))) |
| 47 | 46 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (π β π’ β (βπ β (π« π’ β© Fin) Β¬ π = βͺ π β Β¬ π = βͺ (π₯ β© π’)))) |
| 48 | 47 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β (π β π’ β (βπ β (π« π’ β© Fin) Β¬ π = βͺ π β Β¬ π = βͺ (π₯ β© π’)))) |
| 49 | 48 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ π’ β π« (fiβπ₯)) β (π β π’ β (βπ β (π« π’ β© Fin) Β¬ π = βͺ π β Β¬ π = βͺ (π₯ β© π’)))) |
| 50 | 49 | impd 410 |
. . . . . . . . . . . . . . . . . 18
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ π’ β π« (fiβπ₯)) β ((π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π) β Β¬ π = βͺ (π₯ β© π’))) |
| 51 | 50 | impr 454 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β Β¬ π = βͺ
(π₯ β© π’)) |
| 52 | 20 | unissi 4917 |
. . . . . . . . . . . . . . . . . . 19
β’ βͺ (π₯
β© π’) β βͺ π₯ |
| 53 | | fiuni 9427 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ β V β βͺ π₯ =
βͺ (fiβπ₯)) |
| 54 | 53 | elv 3479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ βͺ π₯ =
βͺ (fiβπ₯) |
| 55 | | fibas 22701 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(fiβπ₯) β
TopBases |
| 56 | | unitg 22691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((fiβπ₯) β
TopBases β βͺ (topGenβ(fiβπ₯)) = βͺ (fiβπ₯)) |
| 57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ βͺ (topGenβ(fiβπ₯)) = βͺ
(fiβπ₯) |
| 58 | 54, 57 | eqtr4i 2762 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ βͺ π₯ =
βͺ (topGenβ(fiβπ₯)) |
| 59 | | unieq 4919 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π½ = (topGenβ(fiβπ₯)) β βͺ π½ =
βͺ (topGenβ(fiβπ₯))) |
| 60 | 58, 59 | eqtr4id 2790 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π½ = (topGenβ(fiβπ₯)) β βͺ π₯ =
βͺ π½) |
| 61 | 60, 2 | eqtr4di 2789 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π½ = (topGenβ(fiβπ₯)) β βͺ π₯ =
π) |
| 62 | 61 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β βͺ π₯ =
π) |
| 63 | 62 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β βͺ π₯ =
π) |
| 64 | 52, 63 | sseqtrid 4034 |
. . . . . . . . . . . . . . . . . 18
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β βͺ (π₯
β© π’) β π) |
| 65 | | eqcom 2738 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = βͺ
(π₯ β© π’) β βͺ (π₯ β© π’) = π) |
| 66 | | eqss 3997 |
. . . . . . . . . . . . . . . . . . . 20
β’ (βͺ (π₯
β© π’) = π β (βͺ (π₯
β© π’) β π β§ π β βͺ (π₯ β© π’))) |
| 67 | 66 | baib 535 |
. . . . . . . . . . . . . . . . . . 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 3989 |
. . . . . . . . . . . . . . . . 17
β’ (π β βͺ π’
β (βͺ π’ β βͺ (π₯ β© π’) β π β βͺ (π₯ β© π’))) |
| 72 | 71 | con3rr3 155 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π β βͺ (π₯
β© π’) β (π β βͺ π’
β Β¬ βͺ π’ β βͺ (π₯ β© π’))) |
| 73 | 70, 72 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (π β βͺ π’ β Β¬ βͺ π’
β βͺ (π₯ β© π’))) |
| 74 | | nss 4046 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
βͺ π’ β βͺ (π₯ β© π’) β βπ¦(π¦ β βͺ π’ β§ Β¬ π¦ β βͺ (π₯ β© π’))) |
| 75 | | df-rex 3070 |
. . . . . . . . . . . . . . . . 17
β’
(βπ¦ β
βͺ π’ Β¬ π¦ β βͺ (π₯ β© π’) β βπ¦(π¦ β βͺ π’ β§ Β¬ π¦ β βͺ (π₯ β© π’))) |
| 76 | 74, 75 | bitr4i 278 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
βͺ π’ β βͺ (π₯ β© π’) β βπ¦ β βͺ π’ Β¬ π¦ β βͺ (π₯ β© π’)) |
| 77 | | eluni2 4912 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β βͺ π’
β βπ€ β
π’ π¦ β π€) |
| 78 | | elpwi 4609 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π’ β π«
(fiβπ₯) β π’ β (fiβπ₯)) |
| 79 | 78 | sseld 3981 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π’ β π«
(fiβπ₯) β (π€ β π’ β π€ β (fiβπ₯))) |
| 80 | 79 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (π€ β π’ β π€ β (fiβπ₯))) |
| 81 | | elfi 9412 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π€ β V β§ π₯ β V) β (π€ β (fiβπ₯) β βπ‘ β (π« π₯ β© Fin)π€ = β© π‘)) |
| 82 | 81 | el2v 3481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β (fiβπ₯) β βπ‘ β (π« π₯ β© Fin)π€ = β© π‘) |
| 83 | 80, 82 | imbitrdi 250 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β (π€ β π’ β βπ‘ β (π« π₯ β© Fin)π€ = β© π‘)) |
| 84 | 2 | alexsubALTlem3 23774 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β βπ β π‘ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π) |
| 85 | 78 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π’ β π«
(fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) β π’ β (fiβπ₯)) |
| 86 | 85 | ad4antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π’ β (fiβπ₯)) |
| 87 | | ssfii 9418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π₯ β V β π₯ β (fiβπ₯)) |
| 88 | 87 | elv 3479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ π₯ β (fiβπ₯) |
| 89 | | elinel1 4195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π‘ β (π« π₯ β© Fin) β π‘ β π« π₯) |
| 90 | 89 | elpwid 4611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π‘ β (π« π₯ β© Fin) β π‘ β π₯) |
| 91 | 90 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π‘ β (π« π₯ β© Fin) β§ π€ = β©
π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’))) β π‘ β π₯) |
| 92 | 91 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π‘ β π₯) |
| 93 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π β π‘) |
| 94 | 92, 93 | sseldd 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π β π₯) |
| 95 | 88, 94 | sselid 3980 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π β (fiβπ₯)) |
| 96 | 95 | snssd 4812 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β {π } β (fiβπ₯)) |
| 97 | 86, 96 | unssd 4186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β (π’ βͺ {π }) β (fiβπ₯)) |
| 98 | | fvex 6904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(fiβπ₯) β
V |
| 99 | 98 | elpw2 5345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π’ βͺ {π }) β π« (fiβπ₯) β (π’ βͺ {π }) β (fiβπ₯)) |
| 100 | 97, 99 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β (π’ βͺ {π }) β π« (fiβπ₯)) |
| 101 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π’ β π«
(fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) β π β π’) |
| 102 | 101 | ad4antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π β π’) |
| 103 | | ssun1 4172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ π’ β (π’ βͺ {π }) |
| 104 | 102, 103 | sstrdi 3994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π β (π’ βͺ {π })) |
| 105 | | unieq 4919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = π β βͺ π = βͺ
π) |
| 106 | 105 | eqeq2d 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = π β (π = βͺ π β π = βͺ π)) |
| 107 | 106 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = π β (Β¬ π = βͺ π β Β¬ π = βͺ π)) |
| 108 | 107 | cbvralvw 3233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(βπ β
(π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ
π β βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π) |
| 109 | 108 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(βπ β
(π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ
π β βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π) |
| 110 | 109 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π) |
| 111 | 100, 104,
110 | jca32 515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β ((π’ βͺ {π }) β π« (fiβπ₯) β§ (π β (π’ βͺ {π }) β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) |
| 112 | | sseq2 4008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π§ = (π’ βͺ {π }) β (π β π§ β π β (π’ βͺ {π }))) |
| 113 | | pweq 4616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π§ = (π’ βͺ {π }) β π« π§ = π« (π’ βͺ {π })) |
| 114 | 113 | ineq1d 4211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π§ = (π’ βͺ {π }) β (π« π§ β© Fin) = (π« (π’ βͺ {π }) β© Fin)) |
| 115 | 114 | raleqdv 3324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π§ = (π’ βͺ {π }) β (βπ β (π« π§ β© Fin) Β¬ π = βͺ π β βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) |
| 116 | 112, 115 | anbi12d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π§ = (π’ βͺ {π }) β ((π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π) β (π β (π’ βͺ {π }) β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) |
| 117 | 116 | elrab 3683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π’ βͺ {π }) β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β ((π’ βͺ {π }) β π« (fiβπ₯) β§ (π β (π’ βͺ {π }) β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) |
| 118 | 111, 117 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β (π’ βͺ {π }) β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) |
| 119 | | elun1 4176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π’ βͺ {π }) β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β (π’ βͺ {π }) β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ
{β
})) |
| 120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β (π’ βͺ {π }) β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ
{β
})) |
| 121 | | vsnid 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ π β {π } |
| 122 | | elun2 4177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β {π } β π β (π’ βͺ {π })) |
| 123 | 121, 122 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ π β (π’ βͺ {π }) |
| 124 | | intss1 4967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (π β π‘ β β© π‘ β π ) |
| 125 | | sseq1 4007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (π€ = β©
π‘ β (π€ β π β β© π‘ β π )) |
| 126 | 124, 125 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (π β π‘ β (π€ = β© π‘ β π€ β π )) |
| 127 | 126 | impcom 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π€ = β©
π‘ β§ π β π‘) β π€ β π ) |
| 128 | 127 | ad4ant24 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((((π‘ β (π« π₯ β© Fin) β§ π€ = β©
π‘) β§ π¦ β π€) β§ π β π‘) β π€ β π ) |
| 129 | 128 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π€ β π’ β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ π β π‘)) β π€ β π ) |
| 130 | 129 | adantrrr 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π€ β π’ β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β π€ β π ) |
| 131 | 130 | adantll 711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β π€ β π ) |
| 132 | | simprlr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β π¦ β π€) |
| 133 | 131, 132 | sseldd 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β π¦ β π ) |
| 134 | 90 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (((π‘ β (π« π₯ β© Fin) β§ π€ = β©
π‘) β§ π¦ β π€) β π‘ β π₯) |
| 135 | 134 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β π‘ β π₯) |
| 136 | | simprrl 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β π β π‘) |
| 137 | 135, 136 | sseldd 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ (((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ π¦ β π€) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π))) β π β π₯) |
| 138 | | elin 3964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β (π₯ β© π’) β (π β π₯ β§ π β π’)) |
| 139 | | elunii 4913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π¦ β π β§ π β (π₯ β© π’)) β π¦ β βͺ (π₯ β© π’)) |
| 140 | 139 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π¦ β π β (π β (π₯ β© π’) β π¦ β βͺ (π₯ β© π’))) |
| 141 | 138, 140 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π¦ β π β ((π β π₯ β§ π β π’) β π¦ β βͺ (π₯ β© π’))) |
| 142 | 141 | expd 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 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 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β (π¦ β π€ β (Β¬ π¦ β βͺ (π₯ β© π’) β ((π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π) β Β¬ π β π’))))) |
| 148 | 147 | imp55 442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β Β¬ π β π’) |
| 149 | | vex 3477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ π β V |
| 150 | | eleq1w 2815 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π£ = π β (π£ β (π’ βͺ {π }) β π β (π’ βͺ {π }))) |
| 151 | | elequ1 2112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π£ = π β (π£ β π’ β π β π’)) |
| 152 | 151 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π£ = π β (Β¬ π£ β π’ β Β¬ π β π’)) |
| 153 | 150, 152 | anbi12d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π£ = π β ((π£ β (π’ βͺ {π }) β§ Β¬ π£ β π’) β (π β (π’ βͺ {π }) β§ Β¬ π β π’))) |
| 154 | 149, 153 | spcev 3596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β (π’ βͺ {π }) β§ Β¬ π β π’) β βπ£(π£ β (π’ βͺ {π }) β§ Β¬ π£ β π’)) |
| 155 | 123, 148,
154 | sylancr 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β βπ£(π£ β (π’ βͺ {π }) β§ Β¬ π£ β π’)) |
| 156 | | nss 4046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (Β¬
(π’ βͺ {π }) β π’ β βπ£(π£ β (π’ βͺ {π }) β§ Β¬ π£ β π’)) |
| 157 | 155, 156 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β Β¬ (π’ βͺ {π }) β π’) |
| 158 | | eqimss2 4041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π’ = (π’ βͺ {π }) β (π’ βͺ {π }) β π’) |
| 159 | 158 | necon3bi 2966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (Β¬
(π’ βͺ {π }) β π’ β π’ β (π’ βͺ {π })) |
| 160 | 157, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π’ β (π’ βͺ {π })) |
| 161 | 160, 103 | jctil 519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β (π’ β (π’ βͺ {π }) β§ π’ β (π’ βͺ {π }))) |
| 162 | | df-pss 3967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π’ β (π’ βͺ {π }) β (π’ β (π’ βͺ {π }) β§ π’ β (π’ βͺ {π }))) |
| 163 | 161, 162 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β π’ β (π’ βͺ {π })) |
| 164 | | psseq2 4088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π£ = (π’ βͺ {π }) β (π’ β π£ β π’ β (π’ βͺ {π }))) |
| 165 | 164 | rspcev 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π’ βͺ {π }) β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β§ π’ β (π’ βͺ {π })) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£) |
| 166 | 120, 163,
165 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β§ (π β π‘ β§ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π)) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£) |
| 167 | 84, 166 | rexlimddv 3160 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π½ =
(topGenβ(fiβπ₯))
β§ βπ β
π« π₯(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£) |
| 168 | 167 | exp45 438 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β (π¦ β π€ β (Β¬ π¦ β βͺ (π₯ β© π’) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£)))) |
| 169 | 168 | expd 415 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β (π‘ β (π« π₯ β© Fin) β (π€ = β© π‘ β (π¦ β π€ β (Β¬ π¦ β βͺ (π₯ β© π’) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£))))) |
| 170 | 169 | rexlimdv 3152 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β (βπ‘ β (π« π₯ β© Fin)π€ = β© π‘ β (π¦ β π€ β (Β¬ π¦ β βͺ (π₯ β© π’) β βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})π’ β π£)))) |
| 171 | 170 | ex 412 |
. . . . . . . . . . . . . . . . . . . 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 3152 |
. . . . . . . . . . . . . . . . . 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 3152 |
. . . . . . . . . . . . . . . 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 412 |
. . . . . . . . . . 11
β’ ((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β ((π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) β (βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π = βͺ π))) |
| 181 | 180 | adantr 480 |
. . . . . . . . . 10
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β ((π’ β π«
(fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π)) β (βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π = βͺ π))) |
| 182 | | ssun1 4172 |
. . . . . . . . . . . . . 14
β’ {π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ
{β
}) |
| 183 | | eqimss2 4041 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π β π β π§) |
| 184 | 183 | biantrurd 532 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β (βπ β (π« π§ β© Fin) Β¬ π = βͺ π β (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π))) |
| 185 | | pweq 4616 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = π β π« π§ = π« π) |
| 186 | 185 | ineq1d 4211 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π β (π« π§ β© Fin) = (π« π β© Fin)) |
| 187 | 186 | raleqdv 3324 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β (βπ β (π« π§ β© Fin) Β¬ π = βͺ π β βπ β (π« π β© Fin) Β¬ π = βͺ
π)) |
| 188 | 184, 187 | bitr3d 281 |
. . . . . . . . . . . . . . 15
β’ (π§ = π β ((π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π) β βπ β (π« π β© Fin) Β¬ π = βͺ
π)) |
| 189 | | simpll3 1213 |
. . . . . . . . . . . . . . 15
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β π β π« (fiβπ₯)) |
| 190 | | simplr 766 |
. . . . . . . . . . . . . . 15
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β βπ β (π« π β© Fin) Β¬ π = βͺ π) |
| 191 | 188, 189,
190 | elrabd 3685 |
. . . . . . . . . . . . . 14
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β π β {π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)}) |
| 192 | 182, 191 | sselid 3980 |
. . . . . . . . . . . . 13
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β π β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ
{β
})) |
| 193 | | psseq2 4088 |
. . . . . . . . . . . . . . 15
β’ (π£ = π β (π’ β π£ β π’ β π)) |
| 194 | 193 | notbid 318 |
. . . . . . . . . . . . . 14
β’ (π£ = π β (Β¬ π’ β π£ β Β¬ π’ β π)) |
| 195 | 194 | rspcv 3608 |
. . . . . . . . . . . . 13
β’ (π β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) β
(βπ£ β ({π§ β π«
(fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π’ β π)) |
| 196 | 192, 195 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β (βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π’ β π)) |
| 197 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π = β
β π = β
) |
| 198 | | 0elpw 5354 |
. . . . . . . . . . . . . . . . . 18
β’ β
β π« π |
| 199 | | 0fin 9175 |
. . . . . . . . . . . . . . . . . 18
β’ β
β Fin |
| 200 | 198, 199 | elini 4193 |
. . . . . . . . . . . . . . . . 17
β’ β
β (π« π β©
Fin) |
| 201 | 197, 200 | eqeltrdi 2840 |
. . . . . . . . . . . . . . . 16
β’ (π = β
β π β (π« π β© Fin)) |
| 202 | | unieq 4919 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β βͺ π = βͺ
π) |
| 203 | 202 | eqeq2d 2742 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π = βͺ π β π = βͺ π)) |
| 204 | 203 | notbid 318 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (Β¬ π = βͺ π β Β¬ π = βͺ π)) |
| 205 | 204 | rspccv 3609 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
(π« π β© Fin)
Β¬ π = βͺ π
β (π β (π«
π β© Fin) β Β¬
π = βͺ π)) |
| 206 | 201, 205 | syl5 34 |
. . . . . . . . . . . . . . 15
β’
(βπ β
(π« π β© Fin)
Β¬ π = βͺ π
β (π = β
β
Β¬ π = βͺ π)) |
| 207 | 206 | necon2ad 2954 |
. . . . . . . . . . . . . 14
β’
(βπ β
(π« π β© Fin)
Β¬ π = βͺ π
β (π = βͺ π
β π β
β
)) |
| 208 | 207 | ad2antlr 724 |
. . . . . . . . . . . . 13
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β (π = βͺ π β π β β
)) |
| 209 | | psseq1 4087 |
. . . . . . . . . . . . . . 15
β’ (π’ = β
β (π’ β π β β
β π)) |
| 210 | 209 | adantl 481 |
. . . . . . . . . . . . . 14
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β§ π’ = β
) β (π’ β π β β
β π)) |
| 211 | | 0pss 4444 |
. . . . . . . . . . . . . 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 412 |
. . . . . . . . . 10
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β (π’ = β
β (βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π = βͺ π))) |
| 216 | 181, 215 | jaod 856 |
. . . . . . . . 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 3152 |
. . . . . . 7
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β (βπ’ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
})βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β
}) Β¬ π’ β π£ β Β¬ π = βͺ π)) |
| 219 | 3, 218 | mpd 15 |
. . . . . 6
β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ
π) β Β¬ π = βͺ
π) |
| 220 | 219 | ex 412 |
. . . . 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 1118 |
. 2
β’ (π½ = (topGenβ(fiβπ₯)) β (βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β (π β π« (fiβπ₯) β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)))) |
| 224 | 223 | ralrimdv 3151 |
1
β’ (π½ = (topGenβ(fiβπ₯)) β (βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β βπ β π«
(fiβπ₯)(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π))) |
