Step | Hyp | Ref
| Expression |
1 | | prproropreud.b |
. . . 4
β’ (π β π
Or π) |
2 | | prproropreud.o |
. . . . 5
β’ π = (π
β© (π Γ π)) |
3 | | prproropreud.p |
. . . . 5
β’ π = {π β π« π β£ (β―βπ) = 2} |
4 | | eqid 2731 |
. . . . 5
β’ (π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©) = (π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©) |
5 | 2, 3, 4 | prproropf1o 46475 |
. . . 4
β’ (π
Or π β (π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©):πβ1-1-ontoβπ) |
6 | 1, 5 | syl 17 |
. . 3
β’ (π β (π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©):πβ1-1-ontoβπ) |
7 | | sbceq1a 3789 |
. . . 4
β’ (π₯ = ((π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©)βπ¦) β (π β [((π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©)βπ¦) / π₯]π)) |
8 | 7 | adantl 481 |
. . 3
β’ ((π β§ π₯ = ((π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©)βπ¦)) β (π β [((π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©)βπ¦) / π₯]π)) |
9 | | prproropreud.z |
. . 3
β’ (π₯ = π§ β (π β π)) |
10 | | nfsbc1v 3798 |
. . 3
β’
β²π₯[((π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©)βπ¦) / π₯]π |
11 | 6, 8, 9, 10 | reuf1odnf 46115 |
. 2
β’ (π β (β!π₯ β π π β β!π¦ β π [((π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©)βπ¦) / π₯]π)) |
12 | | eqidd 2732 |
. . . . . 6
β’ ((π β§ π¦ β π) β (π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©) = (π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©)) |
13 | | infeq1 9474 |
. . . . . . . 8
β’ (π = π¦ β inf(π, π, π
) = inf(π¦, π, π
)) |
14 | | supeq1 9443 |
. . . . . . . 8
β’ (π = π¦ β sup(π, π, π
) = sup(π¦, π, π
)) |
15 | 13, 14 | opeq12d 4882 |
. . . . . . 7
β’ (π = π¦ β β¨inf(π, π, π
), sup(π, π, π
)β© = β¨inf(π¦, π, π
), sup(π¦, π, π
)β©) |
16 | 15 | adantl 481 |
. . . . . 6
β’ (((π β§ π¦ β π) β§ π = π¦) β β¨inf(π, π, π
), sup(π, π, π
)β© = β¨inf(π¦, π, π
), sup(π¦, π, π
)β©) |
17 | | simpr 484 |
. . . . . 6
β’ ((π β§ π¦ β π) β π¦ β π) |
18 | | opex 5465 |
. . . . . . 7
β’
β¨inf(π¦, π, π
), sup(π¦, π, π
)β© β V |
19 | 18 | a1i 11 |
. . . . . 6
β’ ((π β§ π¦ β π) β β¨inf(π¦, π, π
), sup(π¦, π, π
)β© β V) |
20 | 12, 16, 17, 19 | fvmptd 7006 |
. . . . 5
β’ ((π β§ π¦ β π) β ((π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©)βπ¦) = β¨inf(π¦, π, π
), sup(π¦, π, π
)β©) |
21 | 20 | sbceq1d 3783 |
. . . 4
β’ ((π β§ π¦ β π) β ([((π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©)βπ¦) / π₯]π β [β¨inf(π¦, π, π
), sup(π¦, π, π
)β© / π₯]π)) |
22 | | prproropreud.x |
. . . . . 6
β’ (π₯ = β¨inf(π¦, π, π
), sup(π¦, π, π
)β© β (π β π)) |
23 | 22 | sbcieg 3818 |
. . . . 5
β’
(β¨inf(π¦, π, π
), sup(π¦, π, π
)β© β V β
([β¨inf(π¦, π, π
), sup(π¦, π, π
)β© / π₯]π β π)) |
24 | 19, 23 | syl 17 |
. . . 4
β’ ((π β§ π¦ β π) β ([β¨inf(π¦, π, π
), sup(π¦, π, π
)β© / π₯]π β π)) |
25 | 21, 24 | bitrd 278 |
. . 3
β’ ((π β§ π¦ β π) β ([((π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©)βπ¦) / π₯]π β π)) |
26 | 25 | reubidva 3391 |
. 2
β’ (π β (β!π¦ β π [((π β π β¦ β¨inf(π, π, π
), sup(π, π, π
)β©)βπ¦) / π₯]π β β!π¦ β π π)) |
27 | 11, 26 | bitrd 278 |
1
β’ (π β (β!π₯ β π π β β!π¦ β π π)) |