Step | Hyp | Ref
| Expression |
1 | | dfiun3g 5963 |
. . . 4
β’
(βπ§ β
πΎ πΏ β On β βͺ π§ β πΎ πΏ = βͺ ran (π§ β πΎ β¦ πΏ)) |
2 | 1 | 3ad2ant2 1134 |
. . 3
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β βͺ π§ β πΎ πΏ = βͺ ran (π§ β πΎ β¦ πΏ)) |
3 | 2 | oveq2d 7424 |
. 2
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β (π΄πΉβͺ π§ β πΎ πΏ) = (π΄πΉβͺ ran (π§ β πΎ β¦ πΏ))) |
4 | | simp1 1136 |
. . . 4
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β πΎ β π) |
5 | | mptexg 7222 |
. . . 4
β’ (πΎ β π β (π§ β πΎ β¦ πΏ) β V) |
6 | | rnexg 7894 |
. . . 4
β’ ((π§ β πΎ β¦ πΏ) β V β ran (π§ β πΎ β¦ πΏ) β V) |
7 | 4, 5, 6 | 3syl 18 |
. . 3
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β ran (π§ β πΎ β¦ πΏ) β V) |
8 | | simp2 1137 |
. . . . 5
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β βπ§ β πΎ πΏ β On) |
9 | | eqid 2732 |
. . . . . 6
β’ (π§ β πΎ β¦ πΏ) = (π§ β πΎ β¦ πΏ) |
10 | 9 | fmpt 7109 |
. . . . 5
β’
(βπ§ β
πΎ πΏ β On β (π§ β πΎ β¦ πΏ):πΎβΆOn) |
11 | 8, 10 | sylib 217 |
. . . 4
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β (π§ β πΎ β¦ πΏ):πΎβΆOn) |
12 | 11 | frnd 6725 |
. . 3
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β ran (π§ β πΎ β¦ πΏ) β On) |
13 | | dmmptg 6241 |
. . . . . 6
β’
(βπ§ β
πΎ πΏ β On β dom (π§ β πΎ β¦ πΏ) = πΎ) |
14 | 13 | 3ad2ant2 1134 |
. . . . 5
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β dom (π§ β πΎ β¦ πΏ) = πΎ) |
15 | | simp3 1138 |
. . . . 5
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β πΎ β β
) |
16 | 14, 15 | eqnetrd 3008 |
. . . 4
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β dom (π§ β πΎ β¦ πΏ) β β
) |
17 | | dm0rn0 5924 |
. . . . 5
β’ (dom
(π§ β πΎ β¦ πΏ) = β
β ran (π§ β πΎ β¦ πΏ) = β
) |
18 | 17 | necon3bii 2993 |
. . . 4
β’ (dom
(π§ β πΎ β¦ πΏ) β β
β ran (π§ β πΎ β¦ πΏ) β β
) |
19 | 16, 18 | sylib 217 |
. . 3
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β ran (π§ β πΎ β¦ πΏ) β β
) |
20 | | onovuni.1 |
. . . 4
β’ (Lim
π¦ β (π΄πΉπ¦) = βͺ π₯ β π¦ (π΄πΉπ₯)) |
21 | | onovuni.2 |
. . . 4
β’ ((π₯ β On β§ π¦ β On β§ π₯ β π¦) β (π΄πΉπ₯) β (π΄πΉπ¦)) |
22 | 20, 21 | onovuni 8341 |
. . 3
β’ ((ran
(π§ β πΎ β¦ πΏ) β V β§ ran (π§ β πΎ β¦ πΏ) β On β§ ran (π§ β πΎ β¦ πΏ) β β
) β (π΄πΉβͺ ran (π§ β πΎ β¦ πΏ)) = βͺ
π₯ β ran (π§ β πΎ β¦ πΏ)(π΄πΉπ₯)) |
23 | 7, 12, 19, 22 | syl3anc 1371 |
. 2
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β (π΄πΉβͺ ran (π§ β πΎ β¦ πΏ)) = βͺ
π₯ β ran (π§ β πΎ β¦ πΏ)(π΄πΉπ₯)) |
24 | | oveq2 7416 |
. . . . . . 7
β’ (π₯ = πΏ β (π΄πΉπ₯) = (π΄πΉπΏ)) |
25 | 24 | eleq2d 2819 |
. . . . . 6
β’ (π₯ = πΏ β (π€ β (π΄πΉπ₯) β π€ β (π΄πΉπΏ))) |
26 | 9, 25 | rexrnmptw 7096 |
. . . . 5
β’
(βπ§ β
πΎ πΏ β On β (βπ₯ β ran (π§ β πΎ β¦ πΏ)π€ β (π΄πΉπ₯) β βπ§ β πΎ π€ β (π΄πΉπΏ))) |
27 | 26 | 3ad2ant2 1134 |
. . . 4
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β (βπ₯ β ran (π§ β πΎ β¦ πΏ)π€ β (π΄πΉπ₯) β βπ§ β πΎ π€ β (π΄πΉπΏ))) |
28 | | eliun 5001 |
. . . 4
β’ (π€ β βͺ π₯ β ran (π§ β πΎ β¦ πΏ)(π΄πΉπ₯) β βπ₯ β ran (π§ β πΎ β¦ πΏ)π€ β (π΄πΉπ₯)) |
29 | | eliun 5001 |
. . . 4
β’ (π€ β βͺ π§ β πΎ (π΄πΉπΏ) β βπ§ β πΎ π€ β (π΄πΉπΏ)) |
30 | 27, 28, 29 | 3bitr4g 313 |
. . 3
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β (π€ β βͺ
π₯ β ran (π§ β πΎ β¦ πΏ)(π΄πΉπ₯) β π€ β βͺ
π§ β πΎ (π΄πΉπΏ))) |
31 | 30 | eqrdv 2730 |
. 2
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β βͺ π₯ β ran (π§ β πΎ β¦ πΏ)(π΄πΉπ₯) = βͺ π§ β πΎ (π΄πΉπΏ)) |
32 | 3, 23, 31 | 3eqtrd 2776 |
1
β’ ((πΎ β π β§ βπ§ β πΎ πΏ β On β§ πΎ β β
) β (π΄πΉβͺ π§ β πΎ πΏ) = βͺ
π§ β πΎ (π΄πΉπΏ)) |