Step | Hyp | Ref
| Expression |
1 | | cplem2.1 |
. . 3
β’ π΄ β V |
2 | | scottex 9828 |
. . 3
β’ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)} β V |
3 | 1, 2 | iunex 7906 |
. 2
β’ βͺ π₯ β π΄ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)} β V |
4 | | nfiu1 4993 |
. . . 4
β’
β²π₯βͺ π₯ β π΄ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)} |
5 | 4 | nfeq2 2925 |
. . 3
β’
β²π₯ π¦ = βͺ π₯ β π΄ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)} |
6 | | ineq2 4171 |
. . . . 5
β’ (π¦ = βͺ π₯ β π΄ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)} β (π΅ β© π¦) = (π΅ β© βͺ
π₯ β π΄ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)})) |
7 | 6 | neeq1d 3004 |
. . . 4
β’ (π¦ = βͺ π₯ β π΄ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)} β ((π΅ β© π¦) β β
β (π΅ β© βͺ
π₯ β π΄ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)}) β β
)) |
8 | 7 | imbi2d 341 |
. . 3
β’ (π¦ = βͺ π₯ β π΄ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)} β ((π΅ β β
β (π΅ β© π¦) β β
) β (π΅ β β
β (π΅ β© βͺ
π₯ β π΄ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)}) β β
))) |
9 | 5, 8 | ralbid 3259 |
. 2
β’ (π¦ = βͺ π₯ β π΄ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)} β (βπ₯ β π΄ (π΅ β β
β (π΅ β© π¦) β β
) β βπ₯ β π΄ (π΅ β β
β (π΅ β© βͺ
π₯ β π΄ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)}) β β
))) |
10 | | eqid 2737 |
. . 3
β’ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)} = {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)} |
11 | | eqid 2737 |
. . 3
β’ βͺ π₯ β π΄ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)} = βͺ
π₯ β π΄ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)} |
12 | 10, 11 | cplem1 9832 |
. 2
β’
βπ₯ β
π΄ (π΅ β β
β (π΅ β© βͺ
π₯ β π΄ {π§ β π΅ β£ βπ€ β π΅ (rankβπ§) β (rankβπ€)}) β β
) |
13 | 3, 9, 12 | ceqsexv2d 3500 |
1
β’
βπ¦βπ₯ β π΄ (π΅ β β
β (π΅ β© π¦) β β
) |