Step | Hyp | Ref
| Expression |
1 | | restfn 12692 |
. . . . . 6
β’
βΎt Fn (V Γ V) |
2 | | elex 2749 |
. . . . . 6
β’ (π΅ β π β π΅ β V) |
3 | | elex 2749 |
. . . . . 6
β’ (π΄ β π β π΄ β V) |
4 | | fnovex 5908 |
. . . . . 6
β’ ((
βΎt Fn (V Γ V) β§ π΅ β V β§ π΄ β V) β (π΅ βΎt π΄) β V) |
5 | 1, 2, 3, 4 | mp3an3an 1343 |
. . . . 5
β’ ((π΅ β π β§ π΄ β π) β (π΅ βΎt π΄) β V) |
6 | | eltg3 13560 |
. . . . 5
β’ ((π΅ βΎt π΄) β V β (π₯ β (topGenβ(π΅ βΎt π΄)) β βπ¦(π¦ β (π΅ βΎt π΄) β§ π₯ = βͺ π¦))) |
7 | 5, 6 | syl 14 |
. . . 4
β’ ((π΅ β π β§ π΄ β π) β (π₯ β (topGenβ(π΅ βΎt π΄)) β βπ¦(π¦ β (π΅ βΎt π΄) β§ π₯ = βͺ π¦))) |
8 | | simpll 527 |
. . . . . . . . 9
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β π΅ β π) |
9 | | funmpt 5255 |
. . . . . . . . . 10
β’ Fun
(π₯ β π΅ β¦ (π₯ β© π΄)) |
10 | 9 | a1i 9 |
. . . . . . . . 9
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β Fun (π₯ β π΅ β¦ (π₯ β© π΄))) |
11 | | restval 12694 |
. . . . . . . . . . . 12
β’ ((π΅ β π β§ π΄ β π) β (π΅ βΎt π΄) = ran (π₯ β π΅ β¦ (π₯ β© π΄))) |
12 | 11 | sseq2d 3186 |
. . . . . . . . . . 11
β’ ((π΅ β π β§ π΄ β π) β (π¦ β (π΅ βΎt π΄) β π¦ β ran (π₯ β π΅ β¦ (π₯ β© π΄)))) |
13 | 12 | biimpa 296 |
. . . . . . . . . 10
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β π¦ β ran (π₯ β π΅ β¦ (π₯ β© π΄))) |
14 | | vex 2741 |
. . . . . . . . . . . . 13
β’ π₯ β V |
15 | 14 | inex1 4138 |
. . . . . . . . . . . 12
β’ (π₯ β© π΄) β V |
16 | 15 | rgenw 2532 |
. . . . . . . . . . 11
β’
βπ₯ β
π΅ (π₯ β© π΄) β V |
17 | | eqid 2177 |
. . . . . . . . . . . 12
β’ (π₯ β π΅ β¦ (π₯ β© π΄)) = (π₯ β π΅ β¦ (π₯ β© π΄)) |
18 | 17 | fnmpt 5343 |
. . . . . . . . . . 11
β’
(βπ₯ β
π΅ (π₯ β© π΄) β V β (π₯ β π΅ β¦ (π₯ β© π΄)) Fn π΅) |
19 | | fnima 5335 |
. . . . . . . . . . 11
β’ ((π₯ β π΅ β¦ (π₯ β© π΄)) Fn π΅ β ((π₯ β π΅ β¦ (π₯ β© π΄)) β π΅) = ran (π₯ β π΅ β¦ (π₯ β© π΄))) |
20 | 16, 18, 19 | mp2b 8 |
. . . . . . . . . 10
β’ ((π₯ β π΅ β¦ (π₯ β© π΄)) β π΅) = ran (π₯ β π΅ β¦ (π₯ β© π΄)) |
21 | 13, 20 | sseqtrrdi 3205 |
. . . . . . . . 9
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β π¦ β ((π₯ β π΅ β¦ (π₯ β© π΄)) β π΅)) |
22 | | ssimaexg 5579 |
. . . . . . . . 9
β’ ((π΅ β π β§ Fun (π₯ β π΅ β¦ (π₯ β© π΄)) β§ π¦ β ((π₯ β π΅ β¦ (π₯ β© π΄)) β π΅)) β βπ§(π§ β π΅ β§ π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§))) |
23 | 8, 10, 21, 22 | syl3anc 1238 |
. . . . . . . 8
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β βπ§(π§ β π΅ β§ π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§))) |
24 | | df-ima 4640 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) = ran ((π₯ β π΅ β¦ (π₯ β© π΄)) βΎ π§) |
25 | | resmpt 4956 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β π΅ β ((π₯ β π΅ β¦ (π₯ β© π΄)) βΎ π§) = (π₯ β π§ β¦ (π₯ β© π΄))) |
26 | 25 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β ((π₯ β π΅ β¦ (π₯ β© π΄)) βΎ π§) = (π₯ β π§ β¦ (π₯ β© π΄))) |
27 | 26 | rneqd 4857 |
. . . . . . . . . . . . . . . . 17
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β ran ((π₯ β π΅ β¦ (π₯ β© π΄)) βΎ π§) = ran (π₯ β π§ β¦ (π₯ β© π΄))) |
28 | 24, 27 | eqtrid 2222 |
. . . . . . . . . . . . . . . 16
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) = ran (π₯ β π§ β¦ (π₯ β© π΄))) |
29 | 28 | unieqd 3821 |
. . . . . . . . . . . . . . 15
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β βͺ
((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) = βͺ ran (π₯ β π§ β¦ (π₯ β© π΄))) |
30 | 15 | dfiun3 4887 |
. . . . . . . . . . . . . . 15
β’ βͺ π₯ β π§ (π₯ β© π΄) = βͺ ran (π₯ β π§ β¦ (π₯ β© π΄)) |
31 | 29, 30 | eqtr4di 2228 |
. . . . . . . . . . . . . 14
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β βͺ
((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) = βͺ π₯ β π§ (π₯ β© π΄)) |
32 | | iunin1 3952 |
. . . . . . . . . . . . . 14
β’ βͺ π₯ β π§ (π₯ β© π΄) = (βͺ
π₯ β π§ π₯ β© π΄) |
33 | 31, 32 | eqtrdi 2226 |
. . . . . . . . . . . . 13
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β βͺ
((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) = (βͺ
π₯ β π§ π₯ β© π΄)) |
34 | | tgvalex 12712 |
. . . . . . . . . . . . . . 15
β’ (π΅ β π β (topGenβπ΅) β V) |
35 | 34 | ad2antrr 488 |
. . . . . . . . . . . . . 14
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β (topGenβπ΅) β V) |
36 | | simpr 110 |
. . . . . . . . . . . . . . 15
β’ ((π΅ β π β§ π΄ β π) β π΄ β π) |
37 | 36 | adantr 276 |
. . . . . . . . . . . . . 14
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β π΄ β π) |
38 | | uniiun 3941 |
. . . . . . . . . . . . . . . 16
β’ βͺ π§ =
βͺ π₯ β π§ π₯ |
39 | | eltg3i 13559 |
. . . . . . . . . . . . . . . 16
β’ ((π΅ β π β§ π§ β π΅) β βͺ π§ β (topGenβπ΅)) |
40 | 38, 39 | eqeltrrid 2265 |
. . . . . . . . . . . . . . 15
β’ ((π΅ β π β§ π§ β π΅) β βͺ
π₯ β π§ π₯ β (topGenβπ΅)) |
41 | 40 | adantlr 477 |
. . . . . . . . . . . . . 14
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β βͺ
π₯ β π§ π₯ β (topGenβπ΅)) |
42 | | elrestr 12696 |
. . . . . . . . . . . . . 14
β’
(((topGenβπ΅)
β V β§ π΄ β
π β§ βͺ π₯ β π§ π₯ β (topGenβπ΅)) β (βͺ π₯ β π§ π₯ β© π΄) β ((topGenβπ΅) βΎt π΄)) |
43 | 35, 37, 41, 42 | syl3anc 1238 |
. . . . . . . . . . . . 13
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β (βͺ π₯ β π§ π₯ β© π΄) β ((topGenβπ΅) βΎt π΄)) |
44 | 33, 43 | eqeltrd 2254 |
. . . . . . . . . . . 12
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β βͺ
((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) β ((topGenβπ΅) βΎt π΄)) |
45 | | unieq 3819 |
. . . . . . . . . . . . 13
β’ (π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) β βͺ π¦ = βͺ
((π₯ β π΅ β¦ (π₯ β© π΄)) β π§)) |
46 | 45 | eleq1d 2246 |
. . . . . . . . . . . 12
β’ (π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) β (βͺ π¦ β ((topGenβπ΅) βΎt π΄) β βͺ ((π₯
β π΅ β¦ (π₯ β© π΄)) β π§) β ((topGenβπ΅) βΎt π΄))) |
47 | 44, 46 | syl5ibrcom 157 |
. . . . . . . . . . 11
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β (π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§) β βͺ π¦ β ((topGenβπ΅) βΎt π΄))) |
48 | 47 | expimpd 363 |
. . . . . . . . . 10
β’ ((π΅ β π β§ π΄ β π) β ((π§ β π΅ β§ π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§)) β βͺ π¦ β ((topGenβπ΅) βΎt π΄))) |
49 | 48 | exlimdv 1819 |
. . . . . . . . 9
β’ ((π΅ β π β§ π΄ β π) β (βπ§(π§ β π΅ β§ π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§)) β βͺ π¦ β ((topGenβπ΅) βΎt π΄))) |
50 | 49 | adantr 276 |
. . . . . . . 8
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β (βπ§(π§ β π΅ β§ π¦ = ((π₯ β π΅ β¦ (π₯ β© π΄)) β π§)) β βͺ π¦ β ((topGenβπ΅) βΎt π΄))) |
51 | 23, 50 | mpd 13 |
. . . . . . 7
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β βͺ π¦ β ((topGenβπ΅) βΎt π΄)) |
52 | | eleq1 2240 |
. . . . . . 7
β’ (π₯ = βͺ
π¦ β (π₯ β ((topGenβπ΅) βΎt π΄) β βͺ π¦
β ((topGenβπ΅)
βΎt π΄))) |
53 | 51, 52 | syl5ibrcom 157 |
. . . . . 6
β’ (((π΅ β π β§ π΄ β π) β§ π¦ β (π΅ βΎt π΄)) β (π₯ = βͺ π¦ β π₯ β ((topGenβπ΅) βΎt π΄))) |
54 | 53 | expimpd 363 |
. . . . 5
β’ ((π΅ β π β§ π΄ β π) β ((π¦ β (π΅ βΎt π΄) β§ π₯ = βͺ π¦) β π₯ β ((topGenβπ΅) βΎt π΄))) |
55 | 54 | exlimdv 1819 |
. . . 4
β’ ((π΅ β π β§ π΄ β π) β (βπ¦(π¦ β (π΅ βΎt π΄) β§ π₯ = βͺ π¦) β π₯ β ((topGenβπ΅) βΎt π΄))) |
56 | 7, 55 | sylbid 150 |
. . 3
β’ ((π΅ β π β§ π΄ β π) β (π₯ β (topGenβ(π΅ βΎt π΄)) β π₯ β ((topGenβπ΅) βΎt π΄))) |
57 | 56 | ssrdv 3162 |
. 2
β’ ((π΅ β π β§ π΄ β π) β (topGenβ(π΅ βΎt π΄)) β ((topGenβπ΅) βΎt π΄)) |
58 | | restval 12694 |
. . . 4
β’
(((topGenβπ΅)
β V β§ π΄ β
π) β
((topGenβπ΅)
βΎt π΄) =
ran (π€ β
(topGenβπ΅) β¦
(π€ β© π΄))) |
59 | 34, 36, 58 | syl2an2r 595 |
. . 3
β’ ((π΅ β π β§ π΄ β π) β ((topGenβπ΅) βΎt π΄) = ran (π€ β (topGenβπ΅) β¦ (π€ β© π΄))) |
60 | | eltg3 13560 |
. . . . . . . 8
β’ (π΅ β π β (π€ β (topGenβπ΅) β βπ§(π§ β π΅ β§ π€ = βͺ π§))) |
61 | 60 | adantr 276 |
. . . . . . 7
β’ ((π΅ β π β§ π΄ β π) β (π€ β (topGenβπ΅) β βπ§(π§ β π΅ β§ π€ = βͺ π§))) |
62 | 38 | ineq1i 3333 |
. . . . . . . . . . . 12
β’ (βͺ π§
β© π΄) = (βͺ π₯ β π§ π₯ β© π΄) |
63 | 62, 32 | eqtr4i 2201 |
. . . . . . . . . . 11
β’ (βͺ π§
β© π΄) = βͺ π₯ β π§ (π₯ β© π΄) |
64 | | simplll 533 |
. . . . . . . . . . . . . . . 16
β’ ((((π΅ β π β§ π΄ β π) β§ π§ β π΅) β§ π₯ β π§) β π΅ β π) |
65 | | simpllr 534 |
. . . . . . . . . . . . . . . 16
β’ ((((π΅ β π β§ π΄ β π) β§ π§ β π΅) β§ π₯ β π§) β π΄ β π) |
66 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β π§ β π΅) |
67 | 66 | sselda 3156 |
. . . . . . . . . . . . . . . 16
β’ ((((π΅ β π β§ π΄ β π) β§ π§ β π΅) β§ π₯ β π§) β π₯ β π΅) |
68 | | elrestr 12696 |
. . . . . . . . . . . . . . . 16
β’ ((π΅ β π β§ π΄ β π β§ π₯ β π΅) β (π₯ β© π΄) β (π΅ βΎt π΄)) |
69 | 64, 65, 67, 68 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
β’ ((((π΅ β π β§ π΄ β π) β§ π§ β π΅) β§ π₯ β π§) β (π₯ β© π΄) β (π΅ βΎt π΄)) |
70 | 69 | fmpttd 5672 |
. . . . . . . . . . . . . 14
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β (π₯ β π§ β¦ (π₯ β© π΄)):π§βΆ(π΅ βΎt π΄)) |
71 | 70 | frnd 5376 |
. . . . . . . . . . . . 13
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β ran (π₯ β π§ β¦ (π₯ β© π΄)) β (π΅ βΎt π΄)) |
72 | | eltg3i 13559 |
. . . . . . . . . . . . 13
β’ (((π΅ βΎt π΄) β V β§ ran (π₯ β π§ β¦ (π₯ β© π΄)) β (π΅ βΎt π΄)) β βͺ ran
(π₯ β π§ β¦ (π₯ β© π΄)) β (topGenβ(π΅ βΎt π΄))) |
73 | 5, 71, 72 | syl2an2r 595 |
. . . . . . . . . . . 12
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β βͺ ran
(π₯ β π§ β¦ (π₯ β© π΄)) β (topGenβ(π΅ βΎt π΄))) |
74 | 30, 73 | eqeltrid 2264 |
. . . . . . . . . . 11
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β βͺ
π₯ β π§ (π₯ β© π΄) β (topGenβ(π΅ βΎt π΄))) |
75 | 63, 74 | eqeltrid 2264 |
. . . . . . . . . 10
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β (βͺ π§ β© π΄) β (topGenβ(π΅ βΎt π΄))) |
76 | | ineq1 3330 |
. . . . . . . . . . 11
β’ (π€ = βͺ
π§ β (π€ β© π΄) = (βͺ π§ β© π΄)) |
77 | 76 | eleq1d 2246 |
. . . . . . . . . 10
β’ (π€ = βͺ
π§ β ((π€ β© π΄) β (topGenβ(π΅ βΎt π΄)) β (βͺ
π§ β© π΄) β (topGenβ(π΅ βΎt π΄)))) |
78 | 75, 77 | syl5ibrcom 157 |
. . . . . . . . 9
β’ (((π΅ β π β§ π΄ β π) β§ π§ β π΅) β (π€ = βͺ π§ β (π€ β© π΄) β (topGenβ(π΅ βΎt π΄)))) |
79 | 78 | expimpd 363 |
. . . . . . . 8
β’ ((π΅ β π β§ π΄ β π) β ((π§ β π΅ β§ π€ = βͺ π§) β (π€ β© π΄) β (topGenβ(π΅ βΎt π΄)))) |
80 | 79 | exlimdv 1819 |
. . . . . . 7
β’ ((π΅ β π β§ π΄ β π) β (βπ§(π§ β π΅ β§ π€ = βͺ π§) β (π€ β© π΄) β (topGenβ(π΅ βΎt π΄)))) |
81 | 61, 80 | sylbid 150 |
. . . . . 6
β’ ((π΅ β π β§ π΄ β π) β (π€ β (topGenβπ΅) β (π€ β© π΄) β (topGenβ(π΅ βΎt π΄)))) |
82 | 81 | imp 124 |
. . . . 5
β’ (((π΅ β π β§ π΄ β π) β§ π€ β (topGenβπ΅)) β (π€ β© π΄) β (topGenβ(π΅ βΎt π΄))) |
83 | 82 | fmpttd 5672 |
. . . 4
β’ ((π΅ β π β§ π΄ β π) β (π€ β (topGenβπ΅) β¦ (π€ β© π΄)):(topGenβπ΅)βΆ(topGenβ(π΅ βΎt π΄))) |
84 | 83 | frnd 5376 |
. . 3
β’ ((π΅ β π β§ π΄ β π) β ran (π€ β (topGenβπ΅) β¦ (π€ β© π΄)) β (topGenβ(π΅ βΎt π΄))) |
85 | 59, 84 | eqsstrd 3192 |
. 2
β’ ((π΅ β π β§ π΄ β π) β ((topGenβπ΅) βΎt π΄) β (topGenβ(π΅ βΎt π΄))) |
86 | 57, 85 | eqssd 3173 |
1
β’ ((π΅ β π β§ π΄ β π) β (topGenβ(π΅ βΎt π΄)) = ((topGenβπ΅) βΎt π΄)) |