Step | Hyp | Ref
| Expression |
1 | | ustex2sym 23584 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π£ β π) β βπ€ β π (β‘π€ = π€ β§ (π€ β π€) β π£)) |
2 | 1 | ad4ant13 750 |
. . 3
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π£ β π) β§ (π£ β π£) β π) β βπ€ β π (β‘π€ = π€ β§ (π€ β π€) β π£)) |
3 | | simprl 770 |
. . . . . 6
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ (π€ β π€) β π£)) β β‘π€ = π€) |
4 | | simp-5l 784 |
. . . . . . . . 9
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ (π€ β π€) β π£)) β π β (UnifOnβπ)) |
5 | | simplr 768 |
. . . . . . . . 9
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ (π€ β π€) β π£)) β π€ β π) |
6 | | ustssco 23582 |
. . . . . . . . 9
β’ ((π β (UnifOnβπ) β§ π€ β π) β π€ β (π€ β π€)) |
7 | 4, 5, 6 | syl2anc 585 |
. . . . . . . 8
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ (π€ β π€) β π£)) β π€ β (π€ β π€)) |
8 | | simprr 772 |
. . . . . . . 8
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ (π€ β π€) β π£)) β (π€ β π€) β π£) |
9 | | coss2 5813 |
. . . . . . . . . 10
β’ ((π€ β π€) β π£ β (π€ β (π€ β π€)) β (π€ β π£)) |
10 | 9 | adantl 483 |
. . . . . . . . 9
β’ ((π€ β (π€ β π€) β§ (π€ β π€) β π£) β (π€ β (π€ β π€)) β (π€ β π£)) |
11 | | sstr 3953 |
. . . . . . . . . 10
β’ ((π€ β (π€ β π€) β§ (π€ β π€) β π£) β π€ β π£) |
12 | | coss1 5812 |
. . . . . . . . . 10
β’ (π€ β π£ β (π€ β π£) β (π£ β π£)) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
β’ ((π€ β (π€ β π€) β§ (π€ β π€) β π£) β (π€ β π£) β (π£ β π£)) |
14 | 10, 13 | sstrd 3955 |
. . . . . . . 8
β’ ((π€ β (π€ β π€) β§ (π€ β π€) β π£) β (π€ β (π€ β π€)) β (π£ β π£)) |
15 | 7, 8, 14 | syl2anc 585 |
. . . . . . 7
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ (π€ β π€) β π£)) β (π€ β (π€ β π€)) β (π£ β π£)) |
16 | | simpllr 775 |
. . . . . . 7
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ (π€ β π€) β π£)) β (π£ β π£) β π) |
17 | 15, 16 | sstrd 3955 |
. . . . . 6
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ (π€ β π€) β π£)) β (π€ β (π€ β π€)) β π) |
18 | 3, 17 | jca 513 |
. . . . 5
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ (π€ β π€) β π£)) β (β‘π€ = π€ β§ (π€ β (π€ β π€)) β π)) |
19 | 18 | ex 414 |
. . . 4
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β ((β‘π€ = π€ β§ (π€ β π€) β π£) β (β‘π€ = π€ β§ (π€ β (π€ β π€)) β π))) |
20 | 19 | reximdva 3162 |
. . 3
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π£ β π) β§ (π£ β π£) β π) β (βπ€ β π (β‘π€ = π€ β§ (π€ β π€) β π£) β βπ€ β π (β‘π€ = π€ β§ (π€ β (π€ β π€)) β π))) |
21 | 2, 20 | mpd 15 |
. 2
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π£ β π) β§ (π£ β π£) β π) β βπ€ β π (β‘π€ = π€ β§ (π€ β (π€ β π€)) β π)) |
22 | | ustexhalf 23578 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π) β βπ£ β π (π£ β π£) β π) |
23 | 21, 22 | r19.29a 3156 |
1
β’ ((π β (UnifOnβπ) β§ π β π) β βπ€ β π (β‘π€ = π€ β§ (π€ β (π€ β π€)) β π)) |