Step | Hyp | Ref
| Expression |
1 | | dicval.l |
. . . . 5
β’ β€ =
(leβπΎ) |
2 | | dicval.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
3 | | dicval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | | dicval.p |
. . . . 5
β’ π = ((ocβπΎ)βπ) |
5 | | dicval.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
6 | | dicval.e |
. . . . 5
β’ πΈ = ((TEndoβπΎ)βπ) |
7 | | dicval.i |
. . . . 5
β’ πΌ = ((DIsoCβπΎ)βπ) |
8 | 1, 2, 3, 4, 5, 6, 7 | dicfval 39638 |
. . . 4
β’ ((πΎ β π β§ π β π») β πΌ = (π β {π β π΄ β£ Β¬ π β€ π} β¦ {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)})) |
9 | 8 | adantr 481 |
. . 3
β’ (((πΎ β π β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β πΌ = (π β {π β π΄ β£ Β¬ π β€ π} β¦ {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)})) |
10 | 9 | fveq1d 6844 |
. 2
β’ (((πΎ β π β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (πΌβπ) = ((π β {π β π΄ β£ Β¬ π β€ π} β¦ {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)})βπ)) |
11 | | simpr 485 |
. . . 4
β’ (((πΎ β π β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (π β π΄ β§ Β¬ π β€ π)) |
12 | | breq1 5108 |
. . . . . 6
β’ (π = π β (π β€ π β π β€ π)) |
13 | 12 | notbid 317 |
. . . . 5
β’ (π = π β (Β¬ π β€ π β Β¬ π β€ π)) |
14 | 13 | elrab 3645 |
. . . 4
β’ (π β {π β π΄ β£ Β¬ π β€ π} β (π β π΄ β§ Β¬ π β€ π)) |
15 | 11, 14 | sylibr 233 |
. . 3
β’ (((πΎ β π β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β π β {π β π΄ β£ Β¬ π β€ π}) |
16 | | eqeq2 2748 |
. . . . . . . . 9
β’ (π = π β ((πβπ) = π β (πβπ) = π)) |
17 | 16 | riotabidv 7315 |
. . . . . . . 8
β’ (π = π β (β©π β π (πβπ) = π) = (β©π β π (πβπ) = π)) |
18 | 17 | fveq2d 6846 |
. . . . . . 7
β’ (π = π β (π β(β©π β π (πβπ) = π)) = (π β(β©π β π (πβπ) = π))) |
19 | 18 | eqeq2d 2747 |
. . . . . 6
β’ (π = π β (π = (π β(β©π β π (πβπ) = π)) β π = (π β(β©π β π (πβπ) = π)))) |
20 | 19 | anbi1d 630 |
. . . . 5
β’ (π = π β ((π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ) β (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ))) |
21 | 20 | opabbidv 5171 |
. . . 4
β’ (π = π β {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)} = {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)}) |
22 | | eqid 2736 |
. . . 4
β’ (π β {π β π΄ β£ Β¬ π β€ π} β¦ {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)}) = (π β {π β π΄ β£ Β¬ π β€ π} β¦ {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)}) |
23 | 6 | fvexi 6856 |
. . . . . . . . . 10
β’ πΈ β V |
24 | 23 | uniex 7678 |
. . . . . . . . 9
β’ βͺ πΈ
β V |
25 | 24 | rnex 7849 |
. . . . . . . 8
β’ ran βͺ πΈ
β V |
26 | 25 | uniex 7678 |
. . . . . . 7
β’ βͺ ran βͺ πΈ β V |
27 | 26 | pwex 5335 |
. . . . . 6
β’ π«
βͺ ran βͺ πΈ β V |
28 | 27, 23 | xpex 7687 |
. . . . 5
β’
(π« βͺ ran βͺ
πΈ Γ πΈ) β V |
29 | | simpl 483 |
. . . . . . . . 9
β’ ((π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ) β π = (π β(β©π β π (πβπ) = π))) |
30 | | fvssunirn 6875 |
. . . . . . . . . . 11
β’ (π β(β©π β π (πβπ) = π)) β βͺ ran
π |
31 | | elssuni 4898 |
. . . . . . . . . . . . 13
β’ (π β πΈ β π β βͺ πΈ) |
32 | 31 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ) β π β βͺ πΈ) |
33 | | rnss 5894 |
. . . . . . . . . . . 12
β’ (π β βͺ πΈ
β ran π β ran
βͺ πΈ) |
34 | | uniss 4873 |
. . . . . . . . . . . 12
β’ (ran
π β ran βͺ πΈ
β βͺ ran π β βͺ ran
βͺ πΈ) |
35 | 32, 33, 34 | 3syl 18 |
. . . . . . . . . . 11
β’ ((π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ) β βͺ ran
π β βͺ ran βͺ πΈ) |
36 | 30, 35 | sstrid 3955 |
. . . . . . . . . 10
β’ ((π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ) β (π β(β©π β π (πβπ) = π)) β βͺ ran
βͺ πΈ) |
37 | 26 | elpw2 5302 |
. . . . . . . . . 10
β’ ((π β(β©π β π (πβπ) = π)) β π« βͺ ran βͺ πΈ β (π β(β©π β π (πβπ) = π)) β βͺ ran
βͺ πΈ) |
38 | 36, 37 | sylibr 233 |
. . . . . . . . 9
β’ ((π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ) β (π β(β©π β π (πβπ) = π)) β π« βͺ ran βͺ πΈ) |
39 | 29, 38 | eqeltrd 2837 |
. . . . . . . 8
β’ ((π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ) β π β π« βͺ ran βͺ πΈ) |
40 | | simpr 485 |
. . . . . . . 8
β’ ((π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ) β π β πΈ) |
41 | 39, 40 | jca 512 |
. . . . . . 7
β’ ((π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ) β (π β π« βͺ ran βͺ πΈ β§ π β πΈ)) |
42 | 41 | ssopab2i 5507 |
. . . . . 6
β’
{β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)} β {β¨π, π β© β£ (π β π« βͺ ran βͺ πΈ β§ π β πΈ)} |
43 | | df-xp 5639 |
. . . . . 6
β’
(π« βͺ ran βͺ
πΈ Γ πΈ) = {β¨π, π β© β£ (π β π« βͺ ran βͺ πΈ β§ π β πΈ)} |
44 | 42, 43 | sseqtrri 3981 |
. . . . 5
β’
{β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)} β (π« βͺ ran βͺ πΈ Γ πΈ) |
45 | 28, 44 | ssexi 5279 |
. . . 4
β’
{β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)} β V |
46 | 21, 22, 45 | fvmpt 6948 |
. . 3
β’ (π β {π β π΄ β£ Β¬ π β€ π} β ((π β {π β π΄ β£ Β¬ π β€ π} β¦ {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)})βπ) = {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)}) |
47 | 15, 46 | syl 17 |
. 2
β’ (((πΎ β π β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β {π β π΄ β£ Β¬ π β€ π} β¦ {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)})βπ) = {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)}) |
48 | 10, 47 | eqtrd 2776 |
1
β’ (((πΎ β π β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (πΌβπ) = {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)}) |