Step | Hyp | Ref
| Expression |
1 | | tglngval.g |
. . . 4
β’ (π β πΊ β TarskiG) |
2 | | tglngval.p |
. . . . 5
β’ π = (BaseβπΊ) |
3 | | tglngval.l |
. . . . 5
β’ πΏ = (LineGβπΊ) |
4 | | tglngval.i |
. . . . 5
β’ πΌ = (ItvβπΊ) |
5 | 2, 3, 4 | tglng 27530 |
. . . 4
β’ (πΊ β TarskiG β πΏ = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))})) |
6 | 1, 5 | syl 17 |
. . 3
β’ (π β πΏ = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))})) |
7 | 6 | oveqd 7379 |
. 2
β’ (π β (ππΏπ) = (π(π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))})π)) |
8 | | tglngval.x |
. . 3
β’ (π β π β π) |
9 | | tglngval.y |
. . . 4
β’ (π β π β π) |
10 | | tglngval.z |
. . . . 5
β’ (π β π β π) |
11 | 10 | necomd 3000 |
. . . 4
β’ (π β π β π) |
12 | | eldifsn 4752 |
. . . 4
β’ (π β (π β {π}) β (π β π β§ π β π)) |
13 | 9, 11, 12 | sylanbrc 584 |
. . 3
β’ (π β π β (π β {π})) |
14 | 2 | fvexi 6861 |
. . . . 5
β’ π β V |
15 | 14 | rabex 5294 |
. . . 4
β’ {π§ β π β£ (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))} β V |
16 | 15 | a1i 11 |
. . 3
β’ (π β {π§ β π β£ (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))} β V) |
17 | | oveq12 7371 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = π) β (π₯πΌπ¦) = (ππΌπ)) |
18 | 17 | eleq2d 2824 |
. . . . . 6
β’ ((π₯ = π β§ π¦ = π) β (π§ β (π₯πΌπ¦) β π§ β (ππΌπ))) |
19 | | simpl 484 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = π) β π₯ = π) |
20 | | simpr 486 |
. . . . . . . 8
β’ ((π₯ = π β§ π¦ = π) β π¦ = π) |
21 | 20 | oveq2d 7378 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = π) β (π§πΌπ¦) = (π§πΌπ)) |
22 | 19, 21 | eleq12d 2832 |
. . . . . 6
β’ ((π₯ = π β§ π¦ = π) β (π₯ β (π§πΌπ¦) β π β (π§πΌπ))) |
23 | 19 | oveq1d 7377 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = π) β (π₯πΌπ§) = (ππΌπ§)) |
24 | 20, 23 | eleq12d 2832 |
. . . . . 6
β’ ((π₯ = π β§ π¦ = π) β (π¦ β (π₯πΌπ§) β π β (ππΌπ§))) |
25 | 18, 22, 24 | 3orbi123d 1436 |
. . . . 5
β’ ((π₯ = π β§ π¦ = π) β ((π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)) β (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§)))) |
26 | 25 | rabbidv 3418 |
. . . 4
β’ ((π₯ = π β§ π¦ = π) β {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))} = {π§ β π β£ (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))}) |
27 | | sneq 4601 |
. . . . 5
β’ (π₯ = π β {π₯} = {π}) |
28 | 27 | difeq2d 4087 |
. . . 4
β’ (π₯ = π β (π β {π₯}) = (π β {π})) |
29 | | eqid 2737 |
. . . 4
β’ (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) |
30 | 26, 28, 29 | ovmpox 7513 |
. . 3
β’ ((π β π β§ π β (π β {π}) β§ {π§ β π β£ (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))} β V) β (π(π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))})π) = {π§ β π β£ (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))}) |
31 | 8, 13, 16, 30 | syl3anc 1372 |
. 2
β’ (π β (π(π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))})π) = {π§ β π β£ (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))}) |
32 | 7, 31 | eqtrd 2777 |
1
β’ (π β (ππΏπ) = {π§ β π β£ (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))}) |