Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’ βͺ (topGenβ(fiβπ΅)) = βͺ
(topGenβ(fiβπ΅)) |
2 | 1 | iscmp 22755 |
. . . 4
β’
((topGenβ(fiβπ΅)) β Comp β
((topGenβ(fiβπ΅)) β Top β§ βπ₯ β π«
(topGenβ(fiβπ΅))(βͺ
(topGenβ(fiβπ΅))
= βͺ π₯ β βπ¦ β (π« π₯ β© Fin)βͺ
(topGenβ(fiβπ΅))
= βͺ π¦))) |
3 | 2 | simprbi 498 |
. . 3
β’
((topGenβ(fiβπ΅)) β Comp β βπ₯ β π«
(topGenβ(fiβπ΅))(βͺ
(topGenβ(fiβπ΅))
= βͺ π₯ β βπ¦ β (π« π₯ β© Fin)βͺ
(topGenβ(fiβπ΅))
= βͺ π¦)) |
4 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β UFL β§ π = βͺ
π΅) β π = βͺ π΅) |
5 | | elex 3462 |
. . . . . . . . . . . 12
β’ (π β UFL β π β V) |
6 | 5 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β UFL β§ π = βͺ
π΅) β π β V) |
7 | 4, 6 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ ((π β UFL β§ π = βͺ
π΅) β βͺ π΅
β V) |
8 | | uniexb 7699 |
. . . . . . . . . 10
β’ (π΅ β V β βͺ π΅
β V) |
9 | 7, 8 | sylibr 233 |
. . . . . . . . 9
β’ ((π β UFL β§ π = βͺ
π΅) β π΅ β V) |
10 | | fiuni 9369 |
. . . . . . . . 9
β’ (π΅ β V β βͺ π΅ =
βͺ (fiβπ΅)) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
β’ ((π β UFL β§ π = βͺ
π΅) β βͺ π΅ =
βͺ (fiβπ΅)) |
12 | | fibas 22343 |
. . . . . . . . 9
β’
(fiβπ΅) β
TopBases |
13 | | unitg 22333 |
. . . . . . . . 9
β’
((fiβπ΅) β
TopBases β βͺ (topGenβ(fiβπ΅)) = βͺ (fiβπ΅)) |
14 | 12, 13 | mp1i 13 |
. . . . . . . 8
β’ ((π β UFL β§ π = βͺ
π΅) β βͺ (topGenβ(fiβπ΅)) = βͺ
(fiβπ΅)) |
15 | 11, 4, 14 | 3eqtr4d 2783 |
. . . . . . 7
β’ ((π β UFL β§ π = βͺ
π΅) β π = βͺ
(topGenβ(fiβπ΅))) |
16 | 15 | eqeq1d 2735 |
. . . . . 6
β’ ((π β UFL β§ π = βͺ
π΅) β (π = βͺ
π₯ β βͺ (topGenβ(fiβπ΅)) = βͺ π₯)) |
17 | 15 | eqeq1d 2735 |
. . . . . . 7
β’ ((π β UFL β§ π = βͺ
π΅) β (π = βͺ
π¦ β βͺ (topGenβ(fiβπ΅)) = βͺ π¦)) |
18 | 17 | rexbidv 3172 |
. . . . . 6
β’ ((π β UFL β§ π = βͺ
π΅) β (βπ¦ β (π« π₯ β© Fin)π = βͺ π¦ β βπ¦ β (π« π₯ β© Fin)βͺ (topGenβ(fiβπ΅)) = βͺ π¦)) |
19 | 16, 18 | imbi12d 345 |
. . . . 5
β’ ((π β UFL β§ π = βͺ
π΅) β ((π = βͺ
π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) β (βͺ (topGenβ(fiβπ΅)) = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)βͺ (topGenβ(fiβπ΅)) = βͺ π¦))) |
20 | 19 | ralbidv 3171 |
. . . 4
β’ ((π β UFL β§ π = βͺ
π΅) β (βπ₯ β π«
(topGenβ(fiβπ΅))(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) β βπ₯ β π«
(topGenβ(fiβπ΅))(βͺ
(topGenβ(fiβπ΅))
= βͺ π₯ β βπ¦ β (π« π₯ β© Fin)βͺ
(topGenβ(fiβπ΅))
= βͺ π¦))) |
21 | | ssfii 9360 |
. . . . . . . 8
β’ (π΅ β V β π΅ β (fiβπ΅)) |
22 | 9, 21 | syl 17 |
. . . . . . 7
β’ ((π β UFL β§ π = βͺ
π΅) β π΅ β (fiβπ΅)) |
23 | | bastg 22332 |
. . . . . . . 8
β’
((fiβπ΅) β
TopBases β (fiβπ΅) β (topGenβ(fiβπ΅))) |
24 | 12, 23 | ax-mp 5 |
. . . . . . 7
β’
(fiβπ΅) β
(topGenβ(fiβπ΅)) |
25 | 22, 24 | sstrdi 3957 |
. . . . . 6
β’ ((π β UFL β§ π = βͺ
π΅) β π΅ β (topGenβ(fiβπ΅))) |
26 | 25 | sspwd 4574 |
. . . . 5
β’ ((π β UFL β§ π = βͺ
π΅) β π« π΅ β π«
(topGenβ(fiβπ΅))) |
27 | | ssralv 4011 |
. . . . 5
β’
(π« π΅ β
π« (topGenβ(fiβπ΅)) β (βπ₯ β π«
(topGenβ(fiβπ΅))(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) β βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦))) |
28 | 26, 27 | syl 17 |
. . . 4
β’ ((π β UFL β§ π = βͺ
π΅) β (βπ₯ β π«
(topGenβ(fiβπ΅))(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) β βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦))) |
29 | 20, 28 | sylbird 260 |
. . 3
β’ ((π β UFL β§ π = βͺ
π΅) β (βπ₯ β π«
(topGenβ(fiβπ΅))(βͺ
(topGenβ(fiβπ΅))
= βͺ π₯ β βπ¦ β (π« π₯ β© Fin)βͺ
(topGenβ(fiβπ΅))
= βͺ π¦) β βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦))) |
30 | 3, 29 | syl5 34 |
. 2
β’ ((π β UFL β§ π = βͺ
π΅) β
((topGenβ(fiβπ΅)) β Comp β βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦))) |
31 | | simpll 766 |
. . . 4
β’ (((π β UFL β§ π = βͺ
π΅) β§ βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦)) β π β UFL) |
32 | | simplr 768 |
. . . 4
β’ (((π β UFL β§ π = βͺ
π΅) β§ βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦)) β π = βͺ π΅) |
33 | | eqidd 2734 |
. . . 4
β’ (((π β UFL β§ π = βͺ
π΅) β§ βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦)) β
(topGenβ(fiβπ΅))
= (topGenβ(fiβπ΅))) |
34 | | velpw 4566 |
. . . . . . 7
β’ (π§ β π« π΅ β π§ β π΅) |
35 | | unieq 4877 |
. . . . . . . . . . 11
β’ (π₯ = π§ β βͺ π₯ = βͺ
π§) |
36 | 35 | eqeq2d 2744 |
. . . . . . . . . 10
β’ (π₯ = π§ β (π = βͺ π₯ β π = βͺ π§)) |
37 | | pweq 4575 |
. . . . . . . . . . . 12
β’ (π₯ = π§ β π« π₯ = π« π§) |
38 | 37 | ineq1d 4172 |
. . . . . . . . . . 11
β’ (π₯ = π§ β (π« π₯ β© Fin) = (π« π§ β© Fin)) |
39 | 38 | rexeqdv 3313 |
. . . . . . . . . 10
β’ (π₯ = π§ β (βπ¦ β (π« π₯ β© Fin)π = βͺ π¦ β βπ¦ β (π« π§ β© Fin)π = βͺ π¦)) |
40 | 36, 39 | imbi12d 345 |
. . . . . . . . 9
β’ (π₯ = π§ β ((π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) β (π = βͺ π§ β βπ¦ β (π« π§ β© Fin)π = βͺ π¦))) |
41 | 40 | rspccv 3577 |
. . . . . . . 8
β’
(βπ₯ β
π« π΅(π = βͺ
π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) β (π§ β π« π΅ β (π = βͺ π§ β βπ¦ β (π« π§ β© Fin)π = βͺ π¦))) |
42 | 41 | adantl 483 |
. . . . . . 7
β’ (((π β UFL β§ π = βͺ
π΅) β§ βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦)) β (π§ β π« π΅ β (π = βͺ π§ β βπ¦ β (π« π§ β© Fin)π = βͺ π¦))) |
43 | 34, 42 | biimtrrid 242 |
. . . . . 6
β’ (((π β UFL β§ π = βͺ
π΅) β§ βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦)) β (π§ β π΅ β (π = βͺ π§ β βπ¦ β (π« π§ β© Fin)π = βͺ π¦))) |
44 | 43 | imp32 420 |
. . . . 5
β’ ((((π β UFL β§ π = βͺ
π΅) β§ βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦)) β§ (π§ β π΅ β§ π = βͺ π§)) β βπ¦ β (π« π§ β© Fin)π = βͺ π¦) |
45 | | unieq 4877 |
. . . . . . 7
β’ (π¦ = π€ β βͺ π¦ = βͺ
π€) |
46 | 45 | eqeq2d 2744 |
. . . . . 6
β’ (π¦ = π€ β (π = βͺ π¦ β π = βͺ π€)) |
47 | 46 | cbvrexvw 3225 |
. . . . 5
β’
(βπ¦ β
(π« π§ β©
Fin)π = βͺ π¦
β βπ€ β
(π« π§ β©
Fin)π = βͺ π€) |
48 | 44, 47 | sylib 217 |
. . . 4
β’ ((((π β UFL β§ π = βͺ
π΅) β§ βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦)) β§ (π§ β π΅ β§ π = βͺ π§)) β βπ€ β (π« π§ β© Fin)π = βͺ π€) |
49 | 31, 32, 33, 48 | alexsub 23412 |
. . 3
β’ (((π β UFL β§ π = βͺ
π΅) β§ βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦)) β
(topGenβ(fiβπ΅))
β Comp) |
50 | 49 | ex 414 |
. 2
β’ ((π β UFL β§ π = βͺ
π΅) β (βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) β
(topGenβ(fiβπ΅))
β Comp)) |
51 | 30, 50 | impbid 211 |
1
β’ ((π β UFL β§ π = βͺ
π΅) β
((topGenβ(fiβπ΅)) β Comp β βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦))) |