Step | Hyp | Ref
| Expression |
1 | | 0ex 5308 |
. . 3
β’ β
β V |
2 | | eqid 2733 |
. . . 4
β’
(lubββ
) = (lubββ
) |
3 | | eqid 2733 |
. . . 4
β’
(joinββ
) = (joinββ
) |
4 | 2, 3 | joinfval 18326 |
. . 3
β’ (β
β V β (joinββ
) = {β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦} (lubββ
)π§}) |
5 | 1, 4 | ax-mp 5 |
. 2
β’
(joinββ
) = {β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦} (lubββ
)π§} |
6 | | df-oprab 7413 |
. . 3
β’
{β¨β¨π₯,
π¦β©, π§β© β£ {π₯, π¦} (lubββ
)π§} = {π€ β£ βπ₯βπ¦βπ§(π€ = β¨β¨π₯, π¦β©, π§β© β§ {π₯, π¦} (lubββ
)π§)} |
7 | | br0 5198 |
. . . . . . . . 9
β’ Β¬
{π₯, π¦}β
π§ |
8 | | base0 17149 |
. . . . . . . . . . . . 13
β’ β
=
(Baseββ
) |
9 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(leββ
) = (leββ
) |
10 | | biid 261 |
. . . . . . . . . . . . 13
β’
((βπ₯ β
π€ π₯(leββ
)π§ β§ βπ¦ β β
(βπ₯ β π€ π₯(leββ
)π¦ β π§(leββ
)π¦)) β (βπ₯ β π€ π₯(leββ
)π§ β§ βπ¦ β β
(βπ₯ β π€ π₯(leββ
)π¦ β π§(leββ
)π¦))) |
11 | | id 22 |
. . . . . . . . . . . . 13
β’ (β
β V β β
β V) |
12 | 8, 9, 2, 10, 11 | lubfval 18303 |
. . . . . . . . . . . 12
β’ (β
β V β (lubββ
) = ((π€ β π« β
β¦
(β©π§ β
β
(βπ₯ β
π€ π₯(leββ
)π§ β§ βπ¦ β β
(βπ₯ β π€ π₯(leββ
)π¦ β π§(leββ
)π¦)))) βΎ {π€ β£ β!π§ β β
(βπ₯ β π€ π₯(leββ
)π§ β§ βπ¦ β β
(βπ₯ β π€ π₯(leββ
)π¦ β π§(leββ
)π¦))})) |
13 | 1, 12 | ax-mp 5 |
. . . . . . . . . . 11
β’
(lubββ
) = ((π€ β π« β
β¦
(β©π§ β
β
(βπ₯ β
π€ π₯(leββ
)π§ β§ βπ¦ β β
(βπ₯ β π€ π₯(leββ
)π¦ β π§(leββ
)π¦)))) βΎ {π€ β£ β!π§ β β
(βπ₯ β π€ π₯(leββ
)π§ β§ βπ¦ β β
(βπ₯ β π€ π₯(leββ
)π¦ β π§(leββ
)π¦))}) |
14 | | reu0 4359 |
. . . . . . . . . . . . . 14
β’ Β¬
β!π§ β β
(βπ₯ β π€ π₯(leββ
)π§ β§ βπ¦ β β
(βπ₯ β π€ π₯(leββ
)π¦ β π§(leββ
)π¦)) |
15 | 14 | abf 4403 |
. . . . . . . . . . . . 13
β’ {π€ β£ β!π§ β β
(βπ₯ β π€ π₯(leββ
)π§ β§ βπ¦ β β
(βπ₯ β π€ π₯(leββ
)π¦ β π§(leββ
)π¦))} = β
|
16 | 15 | reseq2i 5979 |
. . . . . . . . . . . 12
β’ ((π€ β π« β
β¦ (β©π§
β β
(βπ₯
β π€ π₯(leββ
)π§ β§ βπ¦ β β
(βπ₯ β π€ π₯(leββ
)π¦ β π§(leββ
)π¦)))) βΎ {π€ β£ β!π§ β β
(βπ₯ β π€ π₯(leββ
)π§ β§ βπ¦ β β
(βπ₯ β π€ π₯(leββ
)π¦ β π§(leββ
)π¦))}) = ((π€ β π« β
β¦
(β©π§ β
β
(βπ₯ β
π€ π₯(leββ
)π§ β§ βπ¦ β β
(βπ₯ β π€ π₯(leββ
)π¦ β π§(leββ
)π¦)))) βΎ β
) |
17 | | res0 5986 |
. . . . . . . . . . . 12
β’ ((π€ β π« β
β¦ (β©π§
β β
(βπ₯
β π€ π₯(leββ
)π§ β§ βπ¦ β β
(βπ₯ β π€ π₯(leββ
)π¦ β π§(leββ
)π¦)))) βΎ β
) =
β
|
18 | 16, 17 | eqtri 2761 |
. . . . . . . . . . 11
β’ ((π€ β π« β
β¦ (β©π§
β β
(βπ₯
β π€ π₯(leββ
)π§ β§ βπ¦ β β
(βπ₯ β π€ π₯(leββ
)π¦ β π§(leββ
)π¦)))) βΎ {π€ β£ β!π§ β β
(βπ₯ β π€ π₯(leββ
)π§ β§ βπ¦ β β
(βπ₯ β π€ π₯(leββ
)π¦ β π§(leββ
)π¦))}) = β
|
19 | 13, 18 | eqtri 2761 |
. . . . . . . . . 10
β’
(lubββ
) = β
|
20 | 19 | breqi 5155 |
. . . . . . . . 9
β’ ({π₯, π¦} (lubββ
)π§ β {π₯, π¦}β
π§) |
21 | 7, 20 | mtbir 323 |
. . . . . . . 8
β’ Β¬
{π₯, π¦} (lubββ
)π§ |
22 | 21 | intnan 488 |
. . . . . . 7
β’ Β¬
(π€ = β¨β¨π₯, π¦β©, π§β© β§ {π₯, π¦} (lubββ
)π§) |
23 | 22 | nex 1803 |
. . . . . 6
β’ Β¬
βπ§(π€ = β¨β¨π₯, π¦β©, π§β© β§ {π₯, π¦} (lubββ
)π§) |
24 | 23 | nex 1803 |
. . . . 5
β’ Β¬
βπ¦βπ§(π€ = β¨β¨π₯, π¦β©, π§β© β§ {π₯, π¦} (lubββ
)π§) |
25 | 24 | nex 1803 |
. . . 4
β’ Β¬
βπ₯βπ¦βπ§(π€ = β¨β¨π₯, π¦β©, π§β© β§ {π₯, π¦} (lubββ
)π§) |
26 | 25 | abf 4403 |
. . 3
β’ {π€ β£ βπ₯βπ¦βπ§(π€ = β¨β¨π₯, π¦β©, π§β© β§ {π₯, π¦} (lubββ
)π§)} = β
|
27 | 6, 26 | eqtri 2761 |
. 2
β’
{β¨β¨π₯,
π¦β©, π§β© β£ {π₯, π¦} (lubββ
)π§} = β
|
28 | 5, 27 | eqtri 2761 |
1
β’
(joinββ
) = β
|