Step | Hyp | Ref
| Expression |
1 | | ordtval.1 |
. . . . . 6
β’ π = dom π
|
2 | | dmexg 7896 |
. . . . . 6
β’ (π
β π β dom π
β V) |
3 | 1, 2 | eqeltrid 2835 |
. . . . 5
β’ (π
β π β π β V) |
4 | | unisng 4928 |
. . . . 5
β’ (π β V β βͺ {π}
= π) |
5 | 3, 4 | syl 17 |
. . . 4
β’ (π
β π β βͺ {π} = π) |
6 | 5 | uneq1d 4161 |
. . 3
β’ (π
β π β (βͺ {π} βͺ βͺ (π΄
βͺ π΅)) = (π βͺ βͺ (π΄
βͺ π΅))) |
7 | | ordtval.2 |
. . . . . . 7
β’ π΄ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) |
8 | | ssrab2 4076 |
. . . . . . . . . 10
β’ {π¦ β π β£ Β¬ π¦π
π₯} β π |
9 | 3 | adantr 479 |
. . . . . . . . . . 11
β’ ((π
β π β§ π₯ β π) β π β V) |
10 | | elpw2g 5343 |
. . . . . . . . . . 11
β’ (π β V β ({π¦ β π β£ Β¬ π¦π
π₯} β π« π β {π¦ β π β£ Β¬ π¦π
π₯} β π)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
β’ ((π
β π β§ π₯ β π) β ({π¦ β π β£ Β¬ π¦π
π₯} β π« π β {π¦ β π β£ Β¬ π¦π
π₯} β π)) |
12 | 8, 11 | mpbiri 257 |
. . . . . . . . 9
β’ ((π
β π β§ π₯ β π) β {π¦ β π β£ Β¬ π¦π
π₯} β π« π) |
13 | 12 | fmpttd 7115 |
. . . . . . . 8
β’ (π
β π β (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}):πβΆπ« π) |
14 | 13 | frnd 6724 |
. . . . . . 7
β’ (π
β π β ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) β π« π) |
15 | 7, 14 | eqsstrid 4029 |
. . . . . 6
β’ (π
β π β π΄ β π« π) |
16 | | ordtval.3 |
. . . . . . 7
β’ π΅ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}) |
17 | | ssrab2 4076 |
. . . . . . . . . 10
β’ {π¦ β π β£ Β¬ π₯π
π¦} β π |
18 | | elpw2g 5343 |
. . . . . . . . . . 11
β’ (π β V β ({π¦ β π β£ Β¬ π₯π
π¦} β π« π β {π¦ β π β£ Β¬ π₯π
π¦} β π)) |
19 | 9, 18 | syl 17 |
. . . . . . . . . 10
β’ ((π
β π β§ π₯ β π) β ({π¦ β π β£ Β¬ π₯π
π¦} β π« π β {π¦ β π β£ Β¬ π₯π
π¦} β π)) |
20 | 17, 19 | mpbiri 257 |
. . . . . . . . 9
β’ ((π
β π β§ π₯ β π) β {π¦ β π β£ Β¬ π₯π
π¦} β π« π) |
21 | 20 | fmpttd 7115 |
. . . . . . . 8
β’ (π
β π β (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}):πβΆπ« π) |
22 | 21 | frnd 6724 |
. . . . . . 7
β’ (π
β π β ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}) β π« π) |
23 | 16, 22 | eqsstrid 4029 |
. . . . . 6
β’ (π
β π β π΅ β π« π) |
24 | 15, 23 | unssd 4185 |
. . . . 5
β’ (π
β π β (π΄ βͺ π΅) β π« π) |
25 | | sspwuni 5102 |
. . . . 5
β’ ((π΄ βͺ π΅) β π« π β βͺ (π΄ βͺ π΅) β π) |
26 | 24, 25 | sylib 217 |
. . . 4
β’ (π
β π β βͺ (π΄ βͺ π΅) β π) |
27 | | ssequn2 4182 |
. . . 4
β’ (βͺ (π΄
βͺ π΅) β π β (π βͺ βͺ (π΄ βͺ π΅)) = π) |
28 | 26, 27 | sylib 217 |
. . 3
β’ (π
β π β (π βͺ βͺ (π΄ βͺ π΅)) = π) |
29 | 6, 28 | eqtr2d 2771 |
. 2
β’ (π
β π β π = (βͺ {π} βͺ βͺ (π΄
βͺ π΅))) |
30 | | uniun 4933 |
. 2
β’ βͺ ({π}
βͺ (π΄ βͺ π΅)) = (βͺ {π}
βͺ βͺ (π΄ βͺ π΅)) |
31 | 29, 30 | eqtr4di 2788 |
1
β’ (π
β π β π = βͺ ({π} βͺ (π΄ βͺ π΅))) |