Step | Hyp | Ref
| Expression |
1 | | ustexsym 23583 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π£ β π) β βπ€ β π (β‘π€ = π€ β§ π€ β π£)) |
2 | 1 | ad4ant13 750 |
. . 3
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π£ β π) β§ (π£ β π£) β π) β βπ€ β π (β‘π€ = π€ β§ π€ β π£)) |
3 | | simprl 770 |
. . . . . 6
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π£)) β β‘π€ = π€) |
4 | | coss1 5816 |
. . . . . . . . 9
β’ (π€ β π£ β (π€ β π€) β (π£ β π€)) |
5 | | coss2 5817 |
. . . . . . . . 9
β’ (π€ β π£ β (π£ β π€) β (π£ β π£)) |
6 | 4, 5 | sstrd 3959 |
. . . . . . . 8
β’ (π€ β π£ β (π€ β π€) β (π£ β π£)) |
7 | 6 | ad2antll 728 |
. . . . . . 7
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π£)) β (π€ β π€) β (π£ β π£)) |
8 | | simpllr 775 |
. . . . . . 7
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π£)) β (π£ β π£) β π) |
9 | 7, 8 | sstrd 3959 |
. . . . . 6
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π£)) β (π€ β π€) β π) |
10 | 3, 9 | jca 513 |
. . . . 5
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π£)) β (β‘π€ = π€ β§ (π€ β π€) β π)) |
11 | 10 | ex 414 |
. . . 4
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π£ β π) β§ (π£ β π£) β π) β§ π€ β π) β ((β‘π€ = π€ β§ π€ β π£) β (β‘π€ = π€ β§ (π€ β π€) β π))) |
12 | 11 | reximdva 3166 |
. . 3
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π£ β π) β§ (π£ β π£) β π) β (βπ€ β π (β‘π€ = π€ β§ π€ β π£) β βπ€ β π (β‘π€ = π€ β§ (π€ β π€) β π))) |
13 | 2, 12 | mpd 15 |
. 2
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π£ β π) β§ (π£ β π£) β π) β βπ€ β π (β‘π€ = π€ β§ (π€ β π€) β π)) |
14 | | ustexhalf 23578 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π) β βπ£ β π (π£ β π£) β π) |
15 | 13, 14 | r19.29a 3160 |
1
β’ ((π β (UnifOnβπ) β§ π β π) β βπ€ β π (β‘π€ = π€ β§ (π€ β π€) β π)) |