Step | Hyp | Ref
| Expression |
1 | | mirval.s |
. . 3
β’ π = (pInvGβπΊ) |
2 | | df-mir 27644 |
. . . 4
β’ pInvG =
(π β V β¦ (π₯ β (Baseβπ) β¦ (π¦ β (Baseβπ) β¦ (β©π§ β (Baseβπ)((π₯(distβπ)π§) = (π₯(distβπ)π¦) β§ π₯ β (π§(Itvβπ)π¦)))))) |
3 | | fveq2 6846 |
. . . . . 6
β’ (π = πΊ β (Baseβπ) = (BaseβπΊ)) |
4 | | mirval.p |
. . . . . 6
β’ π = (BaseβπΊ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . 5
β’ (π = πΊ β (Baseβπ) = π) |
6 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = πΊ β (distβπ) = (distβπΊ)) |
7 | | mirval.d |
. . . . . . . . . . 11
β’ β =
(distβπΊ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π = πΊ β (distβπ) = β ) |
9 | 8 | oveqd 7378 |
. . . . . . . . 9
β’ (π = πΊ β (π₯(distβπ)π§) = (π₯ β π§)) |
10 | 8 | oveqd 7378 |
. . . . . . . . 9
β’ (π = πΊ β (π₯(distβπ)π¦) = (π₯ β π¦)) |
11 | 9, 10 | eqeq12d 2749 |
. . . . . . . 8
β’ (π = πΊ β ((π₯(distβπ)π§) = (π₯(distβπ)π¦) β (π₯ β π§) = (π₯ β π¦))) |
12 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = πΊ β (Itvβπ) = (ItvβπΊ)) |
13 | | mirval.i |
. . . . . . . . . . 11
β’ πΌ = (ItvβπΊ) |
14 | 12, 13 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π = πΊ β (Itvβπ) = πΌ) |
15 | 14 | oveqd 7378 |
. . . . . . . . 9
β’ (π = πΊ β (π§(Itvβπ)π¦) = (π§πΌπ¦)) |
16 | 15 | eleq2d 2820 |
. . . . . . . 8
β’ (π = πΊ β (π₯ β (π§(Itvβπ)π¦) β π₯ β (π§πΌπ¦))) |
17 | 11, 16 | anbi12d 632 |
. . . . . . 7
β’ (π = πΊ β (((π₯(distβπ)π§) = (π₯(distβπ)π¦) β§ π₯ β (π§(Itvβπ)π¦)) β ((π₯ β π§) = (π₯ β π¦) β§ π₯ β (π§πΌπ¦)))) |
18 | 5, 17 | riotaeqbidv 7320 |
. . . . . 6
β’ (π = πΊ β (β©π§ β (Baseβπ)((π₯(distβπ)π§) = (π₯(distβπ)π¦) β§ π₯ β (π§(Itvβπ)π¦))) = (β©π§ β π ((π₯ β π§) = (π₯ β π¦) β§ π₯ β (π§πΌπ¦)))) |
19 | 5, 18 | mpteq12dv 5200 |
. . . . 5
β’ (π = πΊ β (π¦ β (Baseβπ) β¦ (β©π§ β (Baseβπ)((π₯(distβπ)π§) = (π₯(distβπ)π¦) β§ π₯ β (π§(Itvβπ)π¦)))) = (π¦ β π β¦ (β©π§ β π ((π₯ β π§) = (π₯ β π¦) β§ π₯ β (π§πΌπ¦))))) |
20 | 5, 19 | mpteq12dv 5200 |
. . . 4
β’ (π = πΊ β (π₯ β (Baseβπ) β¦ (π¦ β (Baseβπ) β¦ (β©π§ β (Baseβπ)((π₯(distβπ)π§) = (π₯(distβπ)π¦) β§ π₯ β (π§(Itvβπ)π¦))))) = (π₯ β π β¦ (π¦ β π β¦ (β©π§ β π ((π₯ β π§) = (π₯ β π¦) β§ π₯ β (π§πΌπ¦)))))) |
21 | | mirval.g |
. . . . 5
β’ (π β πΊ β TarskiG) |
22 | 21 | elexd 3467 |
. . . 4
β’ (π β πΊ β V) |
23 | 4 | fvexi 6860 |
. . . . . 6
β’ π β V |
24 | 23 | mptex 7177 |
. . . . 5
β’ (π₯ β π β¦ (π¦ β π β¦ (β©π§ β π ((π₯ β π§) = (π₯ β π¦) β§ π₯ β (π§πΌπ¦))))) β V |
25 | 24 | a1i 11 |
. . . 4
β’ (π β (π₯ β π β¦ (π¦ β π β¦ (β©π§ β π ((π₯ β π§) = (π₯ β π¦) β§ π₯ β (π§πΌπ¦))))) β V) |
26 | 2, 20, 22, 25 | fvmptd3 6975 |
. . 3
β’ (π β (pInvGβπΊ) = (π₯ β π β¦ (π¦ β π β¦ (β©π§ β π ((π₯ β π§) = (π₯ β π¦) β§ π₯ β (π§πΌπ¦)))))) |
27 | 1, 26 | eqtrid 2785 |
. 2
β’ (π β π = (π₯ β π β¦ (π¦ β π β¦ (β©π§ β π ((π₯ β π§) = (π₯ β π¦) β§ π₯ β (π§πΌπ¦)))))) |
28 | | simpll 766 |
. . . . . . . 8
β’ (((π₯ = π΄ β§ π¦ β π) β§ π§ β π) β π₯ = π΄) |
29 | 28 | oveq1d 7376 |
. . . . . . 7
β’ (((π₯ = π΄ β§ π¦ β π) β§ π§ β π) β (π₯ β π§) = (π΄ β π§)) |
30 | 28 | oveq1d 7376 |
. . . . . . 7
β’ (((π₯ = π΄ β§ π¦ β π) β§ π§ β π) β (π₯ β π¦) = (π΄ β π¦)) |
31 | 29, 30 | eqeq12d 2749 |
. . . . . 6
β’ (((π₯ = π΄ β§ π¦ β π) β§ π§ β π) β ((π₯ β π§) = (π₯ β π¦) β (π΄ β π§) = (π΄ β π¦))) |
32 | 28 | eleq1d 2819 |
. . . . . 6
β’ (((π₯ = π΄ β§ π¦ β π) β§ π§ β π) β (π₯ β (π§πΌπ¦) β π΄ β (π§πΌπ¦))) |
33 | 31, 32 | anbi12d 632 |
. . . . 5
β’ (((π₯ = π΄ β§ π¦ β π) β§ π§ β π) β (((π₯ β π§) = (π₯ β π¦) β§ π₯ β (π§πΌπ¦)) β ((π΄ β π§) = (π΄ β π¦) β§ π΄ β (π§πΌπ¦)))) |
34 | 33 | riotabidva 7337 |
. . . 4
β’ ((π₯ = π΄ β§ π¦ β π) β (β©π§ β π ((π₯ β π§) = (π₯ β π¦) β§ π₯ β (π§πΌπ¦))) = (β©π§ β π ((π΄ β π§) = (π΄ β π¦) β§ π΄ β (π§πΌπ¦)))) |
35 | 34 | mpteq2dva 5209 |
. . 3
β’ (π₯ = π΄ β (π¦ β π β¦ (β©π§ β π ((π₯ β π§) = (π₯ β π¦) β§ π₯ β (π§πΌπ¦)))) = (π¦ β π β¦ (β©π§ β π ((π΄ β π§) = (π΄ β π¦) β§ π΄ β (π§πΌπ¦))))) |
36 | 35 | adantl 483 |
. 2
β’ ((π β§ π₯ = π΄) β (π¦ β π β¦ (β©π§ β π ((π₯ β π§) = (π₯ β π¦) β§ π₯ β (π§πΌπ¦)))) = (π¦ β π β¦ (β©π§ β π ((π΄ β π§) = (π΄ β π¦) β§ π΄ β (π§πΌπ¦))))) |
37 | | mirval.a |
. 2
β’ (π β π΄ β π) |
38 | 23 | mptex 7177 |
. . 3
β’ (π¦ β π β¦ (β©π§ β π ((π΄ β π§) = (π΄ β π¦) β§ π΄ β (π§πΌπ¦)))) β V |
39 | 38 | a1i 11 |
. 2
β’ (π β (π¦ β π β¦ (β©π§ β π ((π΄ β π§) = (π΄ β π¦) β§ π΄ β (π§πΌπ¦)))) β V) |
40 | 27, 36, 37, 39 | fvmptd 6959 |
1
β’ (π β (πβπ΄) = (π¦ β π β¦ (β©π§ β π ((π΄ β π§) = (π΄ β π¦) β§ π΄ β (π§πΌπ¦))))) |