Step | Hyp | Ref
| Expression |
1 | | breq1 5113 |
. . 3
β’ (π = π‘ β (π β€ (π β¨ π) β π‘ β€ (π β¨ π))) |
2 | | oveq1 7369 |
. . . . . . . . . . . 12
β’ (π = π‘ β (π β¨ π§) = (π‘ β¨ π§)) |
3 | 2 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π = π‘ β ((π β¨ π§) β§ π) = ((π‘ β¨ π§) β§ π)) |
4 | 3 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = π‘ β (π β¨ ((π β¨ π§) β§ π)) = (π β¨ ((π‘ β¨ π§) β§ π))) |
5 | 4 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = π‘ β ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π)))) |
6 | | cdleme27.n |
. . . . . . . . 9
β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) |
7 | | cdleme27.o |
. . . . . . . . 9
β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) |
8 | 5, 6, 7 | 3eqtr4g 2802 |
. . . . . . . 8
β’ (π = π‘ β π = π) |
9 | 8 | eqeq2d 2748 |
. . . . . . 7
β’ (π = π‘ β (π’ = π β π’ = π)) |
10 | 9 | imbi2d 341 |
. . . . . 6
β’ (π = π‘ β (((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π) β ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π))) |
11 | 10 | ralbidv 3175 |
. . . . 5
β’ (π = π‘ β (βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π) β βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π))) |
12 | 11 | riotabidv 7320 |
. . . 4
β’ (π = π‘ β (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π))) |
13 | | cdleme27.d |
. . . 4
β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) |
14 | | cdleme27.e |
. . . 4
β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) |
15 | 12, 13, 14 | 3eqtr4g 2802 |
. . 3
β’ (π = π‘ β π· = πΈ) |
16 | | oveq1 7369 |
. . . . 5
β’ (π = π‘ β (π β¨ π) = (π‘ β¨ π)) |
17 | | oveq2 7370 |
. . . . . . 7
β’ (π = π‘ β (π β¨ π ) = (π β¨ π‘)) |
18 | 17 | oveq1d 7377 |
. . . . . 6
β’ (π = π‘ β ((π β¨ π ) β§ π) = ((π β¨ π‘) β§ π)) |
19 | 18 | oveq2d 7378 |
. . . . 5
β’ (π = π‘ β (π β¨ ((π β¨ π ) β§ π)) = (π β¨ ((π β¨ π‘) β§ π))) |
20 | 16, 19 | oveq12d 7380 |
. . . 4
β’ (π = π‘ β ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π)))) |
21 | | cdleme27.f |
. . . 4
β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) |
22 | | cdleme27.g |
. . . 4
β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) |
23 | 20, 21, 22 | 3eqtr4g 2802 |
. . 3
β’ (π = π‘ β πΉ = πΊ) |
24 | 1, 15, 23 | ifbieq12d 4519 |
. 2
β’ (π = π‘ β if(π β€ (π β¨ π), π·, πΉ) = if(π‘ β€ (π β¨ π), πΈ, πΊ)) |
25 | | cdleme27.c |
. 2
β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) |
26 | | cdleme27.y |
. 2
β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) |
27 | 24, 25, 26 | 3eqtr4g 2802 |
1
β’ (π = π‘ β πΆ = π) |