Step | Hyp | Ref
| Expression |
1 | | dicval.i |
. . 3
β’ πΌ = ((DIsoCβπΎ)βπ) |
2 | | dicval.l |
. . . . 5
β’ β€ =
(leβπΎ) |
3 | | dicval.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
4 | | dicval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
5 | 2, 3, 4 | dicffval 39666 |
. . . 4
β’ (πΎ β π β (DIsoCβπΎ) = (π€ β π» β¦ (π β {π β π΄ β£ Β¬ π β€ π€} β¦ {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπΎ)βπ€)(πβ((ocβπΎ)βπ€)) = π)) β§ π β ((TEndoβπΎ)βπ€))}))) |
6 | 5 | fveq1d 6849 |
. . 3
β’ (πΎ β π β ((DIsoCβπΎ)βπ) = ((π€ β π» β¦ (π β {π β π΄ β£ Β¬ π β€ π€} β¦ {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπΎ)βπ€)(πβ((ocβπΎ)βπ€)) = π)) β§ π β ((TEndoβπΎ)βπ€))}))βπ)) |
7 | 1, 6 | eqtrid 2789 |
. 2
β’ (πΎ β π β πΌ = ((π€ β π» β¦ (π β {π β π΄ β£ Β¬ π β€ π€} β¦ {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπΎ)βπ€)(πβ((ocβπΎ)βπ€)) = π)) β§ π β ((TEndoβπΎ)βπ€))}))βπ)) |
8 | | breq2 5114 |
. . . . . 6
β’ (π€ = π β (π β€ π€ β π β€ π)) |
9 | 8 | notbid 318 |
. . . . 5
β’ (π€ = π β (Β¬ π β€ π€ β Β¬ π β€ π)) |
10 | 9 | rabbidv 3418 |
. . . 4
β’ (π€ = π β {π β π΄ β£ Β¬ π β€ π€} = {π β π΄ β£ Β¬ π β€ π}) |
11 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π€ = π β ((LTrnβπΎ)βπ€) = ((LTrnβπΎ)βπ)) |
12 | | dicval.t |
. . . . . . . . . 10
β’ π = ((LTrnβπΎ)βπ) |
13 | 11, 12 | eqtr4di 2795 |
. . . . . . . . 9
β’ (π€ = π β ((LTrnβπΎ)βπ€) = π) |
14 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π€ = π β ((ocβπΎ)βπ€) = ((ocβπΎ)βπ)) |
15 | | dicval.p |
. . . . . . . . . . 11
β’ π = ((ocβπΎ)βπ) |
16 | 14, 15 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π€ = π β ((ocβπΎ)βπ€) = π) |
17 | 16 | fveqeq2d 6855 |
. . . . . . . . 9
β’ (π€ = π β ((πβ((ocβπΎ)βπ€)) = π β (πβπ) = π)) |
18 | 13, 17 | riotaeqbidv 7321 |
. . . . . . . 8
β’ (π€ = π β (β©π β ((LTrnβπΎ)βπ€)(πβ((ocβπΎ)βπ€)) = π) = (β©π β π (πβπ) = π)) |
19 | 18 | fveq2d 6851 |
. . . . . . 7
β’ (π€ = π β (π β(β©π β ((LTrnβπΎ)βπ€)(πβ((ocβπΎ)βπ€)) = π)) = (π β(β©π β π (πβπ) = π))) |
20 | 19 | eqeq2d 2748 |
. . . . . 6
β’ (π€ = π β (π = (π β(β©π β ((LTrnβπΎ)βπ€)(πβ((ocβπΎ)βπ€)) = π)) β π = (π β(β©π β π (πβπ) = π)))) |
21 | | fveq2 6847 |
. . . . . . . 8
β’ (π€ = π β ((TEndoβπΎ)βπ€) = ((TEndoβπΎ)βπ)) |
22 | | dicval.e |
. . . . . . . 8
β’ πΈ = ((TEndoβπΎ)βπ) |
23 | 21, 22 | eqtr4di 2795 |
. . . . . . 7
β’ (π€ = π β ((TEndoβπΎ)βπ€) = πΈ) |
24 | 23 | eleq2d 2824 |
. . . . . 6
β’ (π€ = π β (π β ((TEndoβπΎ)βπ€) β π β πΈ)) |
25 | 20, 24 | anbi12d 632 |
. . . . 5
β’ (π€ = π β ((π = (π β(β©π β ((LTrnβπΎ)βπ€)(πβ((ocβπΎ)βπ€)) = π)) β§ π β ((TEndoβπΎ)βπ€)) β (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ))) |
26 | 25 | opabbidv 5176 |
. . . 4
β’ (π€ = π β {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπΎ)βπ€)(πβ((ocβπΎ)βπ€)) = π)) β§ π β ((TEndoβπΎ)βπ€))} = {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)}) |
27 | 10, 26 | mpteq12dv 5201 |
. . 3
β’ (π€ = π β (π β {π β π΄ β£ Β¬ π β€ π€} β¦ {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπΎ)βπ€)(πβ((ocβπΎ)βπ€)) = π)) β§ π β ((TEndoβπΎ)βπ€))}) = (π β {π β π΄ β£ Β¬ π β€ π} β¦ {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)})) |
28 | | eqid 2737 |
. . 3
β’ (π€ β π» β¦ (π β {π β π΄ β£ Β¬ π β€ π€} β¦ {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπΎ)βπ€)(πβ((ocβπΎ)βπ€)) = π)) β§ π β ((TEndoβπΎ)βπ€))})) = (π€ β π» β¦ (π β {π β π΄ β£ Β¬ π β€ π€} β¦ {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπΎ)βπ€)(πβ((ocβπΎ)βπ€)) = π)) β§ π β ((TEndoβπΎ)βπ€))})) |
29 | 3 | fvexi 6861 |
. . . 4
β’ π΄ β V |
30 | 29 | mptrabex 7180 |
. . 3
β’ (π β {π β π΄ β£ Β¬ π β€ π} β¦ {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)}) β V |
31 | 27, 28, 30 | fvmpt 6953 |
. 2
β’ (π β π» β ((π€ β π» β¦ (π β {π β π΄ β£ Β¬ π β€ π€} β¦ {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπΎ)βπ€)(πβ((ocβπΎ)βπ€)) = π)) β§ π β ((TEndoβπΎ)βπ€))}))βπ) = (π β {π β π΄ β£ Β¬ π β€ π} β¦ {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)})) |
32 | 7, 31 | sylan9eq 2797 |
1
β’ ((πΎ β π β§ π β π») β πΌ = (π β {π β π΄ β£ Β¬ π β€ π} β¦ {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)})) |