Step | Hyp | Ref
| Expression |
1 | | ustexsym 24075 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π£ β π) β βπ€ β π (β‘π€ = π€ β§ π€ β π£)) |
2 | 1 | ad4ant13 748 |
. . 3
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π£ β π) β§ (π£ β π£) β π) β βπ€ β π (β‘π€ = π€ β§ π€ β π£)) |
3 | | simprl 768 |
. . . . . 6
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π£)) β β‘π€ = π€) |
4 | | coss1 5849 |
. . . . . . . . 9
β’ (π€ β π£ β (π€ β π€) β (π£ β π€)) |
5 | | coss2 5850 |
. . . . . . . . 9
β’ (π€ β π£ β (π£ β π€) β (π£ β π£)) |
6 | 4, 5 | sstrd 3987 |
. . . . . . . 8
β’ (π€ β π£ β (π€ β π€) β (π£ β π£)) |
7 | 6 | ad2antll 726 |
. . . . . . 7
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π£)) β (π€ β π€) β (π£ β π£)) |
8 | | simpllr 773 |
. . . . . . 7
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π£)) β (π£ β π£) β π) |
9 | 7, 8 | sstrd 3987 |
. . . . . 6
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π£)) β (π€ β π€) β π) |
10 | 3, 9 | jca 511 |
. . . . 5
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π£)) β (β‘π€ = π€ β§ (π€ β π€) β π)) |
11 | 10 | ex 412 |
. . . 4
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β ((β‘π€ = π€ β§ π€ β π£) β (β‘π€ = π€ β§ (π€ β π€) β π))) |
12 | 11 | reximdva 3162 |
. . 3
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π£ β π) β§ (π£ β π£) β π) β (βπ€ β π (β‘π€ = π€ β§ π€ β π£) β βπ€ β π (β‘π€ = π€ β§ (π€ β π€) β π))) |
13 | 2, 12 | mpd 15 |
. 2
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π£ β π) β§ (π£ β π£) β π) β βπ€ β π (β‘π€ = π€ β§ (π€ β π€) β π)) |
14 | | ustexhalf 24070 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π) β βπ£ β π (π£ β π£) β π) |
15 | 13, 14 | r19.29a 3156 |
1
β’ ((π β (UnifOnβπ) β§ π β π) β βπ€ β π (β‘π€ = π€ β§ (π€ β π€) β π)) |