Step | Hyp | Ref
| Expression |
1 | | ovex 7394 |
. . . . 5
β’ (π΅ βΎt π΄) β V |
2 | | eltg3 22335 |
. . . . 5
β’ ((π΅ βΎt π΄) β V β (π₯ β (topGenβ(π΅ βΎt π΄)) β βπ¦(π¦ β (π΅ βΎt π΄) β§ π₯ = βͺ π¦))) |
3 | 1, 2 | ax-mp 5 |
. . . 4
β’ (π₯ β (topGenβ(π΅ βΎt π΄)) β βπ¦(π¦ β (π΅ βΎt π΄) β§ π₯ = βͺ π¦)) |
4 | | simpll 766 |
. . . . . . . . 9
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β π΅ β π) |
5 | | funmpt 6543 |
. . . . . . . . . 10
β’ Fun
(π₯ β π΅ β¦ (π₯ β© π΄)) |
6 | 5 | a1i 11 |
. . . . . . . . 9
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β Fun (π₯ β π΅ β¦ (π₯ β© π΄))) |
7 | | restval 17316 |
. . . . . . . . . . . 12
β’ ((π΅ β π β§ π΄ β π) β (π΅ βΎt π΄) = ran (π₯ β π΅ β¦ (π₯ β© π΄))) |
8 | 7 | sseq2d 3980 |
. . . . . . . . . . 11
β’ ((π΅ β π β§ π΄ β π) β (π¦ β (π΅ βΎt π΄) β π¦ β ran (π₯ β π΅ β¦ (π₯ β© π΄)))) |
9 | 8 | biimpa 478 |
. . . . . . . . . 10
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β π¦ β ran (π₯ β π΅ β¦ (π₯ β© π΄))) |
10 | | vex 3451 |
. . . . . . . . . . . . 13
β’ π₯ β V |
11 | 10 | inex1 5278 |
. . . . . . . . . . . 12
β’ (π₯ β© π΄) β V |
12 | 11 | rgenw 3065 |
. . . . . . . . . . 11
β’
βπ₯ β
π΅ (π₯ β© π΄) β V |
13 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π₯ β π΅ β¦ (π₯ β© π΄)) = (π₯ β π΅ β¦ (π₯ β© π΄)) |
14 | 13 | fnmpt 6645 |
. . . . . . . . . . 11
β’
(βπ₯ β
π΅ (π₯ β© π΄) β V β (π₯ β π΅ β¦ (π₯ β© π΄)) Fn π΅) |
15 | | fnima 6635 |
. . . . . . . . . . 11
β’ ((π₯ β π΅ β¦ (π₯ β© π΄)) Fn π΅ β ((π₯ β π΅ β¦ (π₯ β© π΄)) β π΅) = ran (π₯ β π΅ β¦ (π₯ β© π΄))) |
16 | 12, 14, 15 | mp2b 10 |
. . . . . . . . . 10
β’ ((π₯ β π΅ β¦ (π₯ β© π΄)) β π΅) = ran (π₯ β π΅ β¦ (π₯ β© π΄)) |
17 | 9, 16 | sseqtrrdi 3999 |
. . . . . . . . 9
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β π¦ β ((π₯ β π΅ β¦ (π₯ β© π΄)) β π΅)) |
18 | | ssimaexg 6931 |
. . . . . . . . 9
β’ ((π΅ β π β§ Fun (π₯ β π΅ β¦ (π₯ β© π΄)) β§ π¦ β ((π₯ β π΅ β¦ (π₯ β© π΄)) β π΅)) β βπ§(π§ β π΅ β§ π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§))) |
19 | 4, 6, 17, 18 | syl3anc 1372 |
. . . . . . . 8
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β βπ§(π§ β π΅ β§ π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§))) |
20 | | df-ima 5650 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) = ran ((π₯ β π΅ β¦ (π₯ β© π΄)) βΎ π§) |
21 | | resmpt 5995 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β π΅ β ((π₯ β π΅ β¦ (π₯ β© π΄)) βΎ π§) = (π₯ β π§ β¦ (π₯ β© π΄))) |
22 | 21 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β ((π₯ β π΅ β¦ (π₯ β© π΄)) βΎ π§) = (π₯ β π§ β¦ (π₯ β© π΄))) |
23 | 22 | rneqd 5897 |
. . . . . . . . . . . . . . . . 17
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β ran ((π₯ β π΅ β¦ (π₯ β© π΄)) βΎ π§) = ran (π₯ β π§ β¦ (π₯ β© π΄))) |
24 | 20, 23 | eqtrid 2785 |
. . . . . . . . . . . . . . . 16
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) = ran (π₯ β π§ β¦ (π₯ β© π΄))) |
25 | 24 | unieqd 4883 |
. . . . . . . . . . . . . . 15
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β βͺ
((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) = βͺ ran (π₯ β π§ β¦ (π₯ β© π΄))) |
26 | 11 | dfiun3 5925 |
. . . . . . . . . . . . . . 15
β’ βͺ π₯ β π§ (π₯ β© π΄) = βͺ ran (π₯ β π§ β¦ (π₯ β© π΄)) |
27 | 25, 26 | eqtr4di 2791 |
. . . . . . . . . . . . . 14
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β βͺ
((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) = βͺ π₯ β π§ (π₯ β© π΄)) |
28 | | iunin1 5036 |
. . . . . . . . . . . . . 14
β’ βͺ π₯ β π§ (π₯ β© π΄) = (βͺ
π₯ β π§ π₯ β© π΄) |
29 | 27, 28 | eqtrdi 2789 |
. . . . . . . . . . . . 13
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β βͺ
((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) = (βͺ
π₯ β π§ π₯ β© π΄)) |
30 | | fvex 6859 |
. . . . . . . . . . . . . 14
β’
(topGenβπ΅)
β V |
31 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π΅ β π β§ π΄ β π) β π΄ β π) |
32 | | uniiun 5022 |
. . . . . . . . . . . . . . . 16
β’ βͺ π§ =
βͺ π₯ β π§ π₯ |
33 | | eltg3i 22334 |
. . . . . . . . . . . . . . . 16
β’ ((π΅ β π β§ π§ β π΅) β βͺ π§ β (topGenβπ΅)) |
34 | 32, 33 | eqeltrrid 2839 |
. . . . . . . . . . . . . . 15
β’ ((π΅ β π β§ π§ β π΅) β βͺ
π₯ β π§ π₯ β (topGenβπ΅)) |
35 | 34 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β βͺ
π₯ β π§ π₯ β (topGenβπ΅)) |
36 | | elrestr 17318 |
. . . . . . . . . . . . . 14
β’
(((topGenβπ΅)
β V β§ π΄ β
π β§ βͺ π₯ β π§ π₯ β (topGenβπ΅)) β (βͺ π₯ β π§ π₯ β© π΄) β ((topGenβπ΅) βΎt π΄)) |
37 | 30, 31, 35, 36 | mp3an2ani 1469 |
. . . . . . . . . . . . 13
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β (βͺ π₯ β π§ π₯ β© π΄) β ((topGenβπ΅) βΎt π΄)) |
38 | 29, 37 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β βͺ
((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) β ((topGenβπ΅) βΎt π΄)) |
39 | | unieq 4880 |
. . . . . . . . . . . . 13
β’ (π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) β βͺ π¦ = βͺ
((π₯ β π΅ β¦ (π₯ β© π΄)) β π§)) |
40 | 39 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) β (βͺ π¦ β ((topGenβπ΅) βΎt π΄) β βͺ ((π₯
β π΅ β¦ (π₯ β© π΄)) β π§) β ((topGenβπ΅) βΎt π΄))) |
41 | 38, 40 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β (π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) β βͺ π¦ β ((topGenβπ΅) βΎt π΄))) |
42 | 41 | expimpd 455 |
. . . . . . . . . 10
β’ ((π΅ β π β§ π΄ β π) β ((π§ β π΅ β§ π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§)) β βͺ π¦ β ((topGenβπ΅) βΎt π΄))) |
43 | 42 | exlimdv 1937 |
. . . . . . . . 9
β’ ((π΅ β π β§ π΄ β π) β (βπ§(π§ β π΅ β§ π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§)) β βͺ π¦ β ((topGenβπ΅) βΎt π΄))) |
44 | 43 | adantr 482 |
. . . . . . . 8
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β (βπ§(π§ β π΅ β§ π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§)) β βͺ π¦ β ((topGenβπ΅) βΎt π΄))) |
45 | 19, 44 | mpd 15 |
. . . . . . 7
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β βͺ π¦ β ((topGenβπ΅) βΎt π΄)) |
46 | | eleq1 2822 |
. . . . . . 7
β’ (π₯ = βͺ
π¦ β (π₯ β ((topGenβπ΅) βΎt π΄) β βͺ π¦
β ((topGenβπ΅)
βΎt π΄))) |
47 | 45, 46 | syl5ibrcom 247 |
. . . . . 6
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β (π₯ = βͺ π¦ β π₯ β ((topGenβπ΅) βΎt π΄))) |
48 | 47 | expimpd 455 |
. . . . 5
β’ ((π΅ β π β§ π΄ β π) β ((π¦ β (π΅ βΎt π΄) β§ π₯ = βͺ π¦) β π₯ β ((topGenβπ΅) βΎt π΄))) |
49 | 48 | exlimdv 1937 |
. . . 4
β’ ((π΅ β π β§ π΄ β π) β (βπ¦(π¦ β (π΅ βΎt π΄) β§ π₯ = βͺ π¦) β π₯ β ((topGenβπ΅) βΎt π΄))) |
50 | 3, 49 | biimtrid 241 |
. . 3
β’ ((π΅ β π β§ π΄ β π) β (π₯ β (topGenβ(π΅ βΎt π΄)) β π₯ β ((topGenβπ΅) βΎt π΄))) |
51 | 50 | ssrdv 3954 |
. 2
β’ ((π΅ β π β§ π΄ β π) β (topGenβ(π΅ βΎt π΄)) β ((topGenβπ΅) βΎt π΄)) |
52 | | restval 17316 |
. . . 4
β’
(((topGenβπ΅)
β V β§ π΄ β
π) β
((topGenβπ΅)
βΎt π΄) =
ran (π€ β
(topGenβπ΅) β¦
(π€ β© π΄))) |
53 | 30, 31, 52 | sylancr 588 |
. . 3
β’ ((π΅ β π β§ π΄ β π) β ((topGenβπ΅) βΎt π΄) = ran (π€ β (topGenβπ΅) β¦ (π€ β© π΄))) |
54 | | eltg3 22335 |
. . . . . . . 8
β’ (π΅ β π β (π€ β (topGenβπ΅) β βπ§(π§ β π΅ β§ π€ = βͺ π§))) |
55 | 54 | adantr 482 |
. . . . . . 7
β’ ((π΅ β π β§ π΄ β π) β (π€ β (topGenβπ΅) β βπ§(π§ β π΅ β§ π€ = βͺ π§))) |
56 | 32 | ineq1i 4172 |
. . . . . . . . . . . 12
β’ (βͺ π§
β© π΄) = (βͺ π₯ β π§ π₯ β© π΄) |
57 | 56, 28 | eqtr4i 2764 |
. . . . . . . . . . 11
β’ (βͺ π§
β© π΄) = βͺ π₯ β π§ (π₯ β© π΄) |
58 | | simplll 774 |
. . . . . . . . . . . . . . . 16
β’ ((((π΅ β π β§ π΄ β π) β§ π§ β π΅) β§ π₯ β π§) β π΅ β π) |
59 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’ ((((π΅ β π β§ π΄ β π) β§ π§ β π΅) β§ π₯ β π§) β π΄ β π) |
60 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β π§ β π΅) |
61 | 60 | sselda 3948 |
. . . . . . . . . . . . . . . 16
β’ ((((π΅ β π β§ π΄ β π) β§ π§ β π΅) β§ π₯ β π§) β π₯ β π΅) |
62 | | elrestr 17318 |
. . . . . . . . . . . . . . . 16
β’ ((π΅ β π β§ π΄ β π β§ π₯ β π΅) β (π₯ β© π΄) β (π΅ βΎt π΄)) |
63 | 58, 59, 61, 62 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π΅ β π β§ π΄ β π) β§ π§ β π΅) β§ π₯ β π§) β (π₯ β© π΄) β (π΅ βΎt π΄)) |
64 | 63 | fmpttd 7067 |
. . . . . . . . . . . . . 14
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β (π₯ β π§ β¦ (π₯ β© π΄)):π§βΆ(π΅ βΎt π΄)) |
65 | 64 | frnd 6680 |
. . . . . . . . . . . . 13
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β ran (π₯ β π§ β¦ (π₯ β© π΄)) β (π΅ βΎt π΄)) |
66 | | eltg3i 22334 |
. . . . . . . . . . . . 13
β’ (((π΅ βΎt π΄) β V β§ ran (π₯ β π§ β¦ (π₯ β© π΄)) β (π΅ βΎt π΄)) β βͺ ran
(π₯ β π§ β¦ (π₯ β© π΄)) β (topGenβ(π΅ βΎt π΄))) |
67 | 1, 65, 66 | sylancr 588 |
. . . . . . . . . . . 12
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β βͺ ran
(π₯ β π§ β¦ (π₯ β© π΄)) β (topGenβ(π΅ βΎt π΄))) |
68 | 26, 67 | eqeltrid 2838 |
. . . . . . . . . . 11
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β βͺ
π₯ β π§ (π₯ β© π΄) β (topGenβ(π΅ βΎt π΄))) |
69 | 57, 68 | eqeltrid 2838 |
. . . . . . . . . 10
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β (βͺ π§ β© π΄) β (topGenβ(π΅ βΎt π΄))) |
70 | | ineq1 4169 |
. . . . . . . . . . 11
β’ (π€ = βͺ
π§ β (π€ β© π΄) = (βͺ π§ β© π΄)) |
71 | 70 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π€ = βͺ
π§ β ((π€ β© π΄) β (topGenβ(π΅ βΎt π΄)) β (βͺ
π§ β© π΄) β (topGenβ(π΅ βΎt π΄)))) |
72 | 69, 71 | syl5ibrcom 247 |
. . . . . . . . 9
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β (π€ = βͺ π§ β (π€ β© π΄) β (topGenβ(π΅ βΎt π΄)))) |
73 | 72 | expimpd 455 |
. . . . . . . 8
β’ ((π΅ β π β§ π΄ β π) β ((π§ β π΅ β§ π€ = βͺ π§) β (π€ β© π΄) β (topGenβ(π΅ βΎt π΄)))) |
74 | 73 | exlimdv 1937 |
. . . . . . 7
β’ ((π΅ β π β§ π΄ β π) β (βπ§(π§ β π΅ β§ π€ = βͺ π§) β (π€ β© π΄) β (topGenβ(π΅ βΎt π΄)))) |
75 | 55, 74 | sylbid 239 |
. . . . . 6
β’ ((π΅ β π β§ π΄ β π) β (π€ β (topGenβπ΅) β (π€ β© π΄) β (topGenβ(π΅ βΎt π΄)))) |
76 | 75 | imp 408 |
. . . . 5
β’ (((π΅ β π β§ π΄ β π) β§ π€ β (topGenβπ΅)) β (π€ β© π΄) β (topGenβ(π΅ βΎt π΄))) |
77 | 76 | fmpttd 7067 |
. . . 4
β’ ((π΅ β π β§ π΄ β π) β (π€ β (topGenβπ΅) β¦ (π€ β© π΄)):(topGenβπ΅)βΆ(topGenβ(π΅ βΎt π΄))) |
78 | 77 | frnd 6680 |
. . 3
β’ ((π΅ β π β§ π΄ β π) β ran (π€ β (topGenβπ΅) β¦ (π€ β© π΄)) β (topGenβ(π΅ βΎt π΄))) |
79 | 53, 78 | eqsstrd 3986 |
. 2
β’ ((π΅ β π β§ π΄ β π) β ((topGenβπ΅) βΎt π΄) β (topGenβ(π΅ βΎt π΄))) |
80 | 51, 79 | eqssd 3965 |
1
β’ ((π΅ β π β§ π΄ β π) β (topGenβ(π΅ βΎt π΄)) = ((topGenβπ΅) βΎt π΄)) |