Step | Hyp | Ref
| Expression |
1 | | tglng.p |
. . . . . . . 8
β’ π = (BaseβπΊ) |
2 | 1 | fvexi 6857 |
. . . . . . 7
β’ π β V |
3 | 2 | rabex 5290 |
. . . . . 6
β’ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))} β V |
4 | 3 | rgen2w 3066 |
. . . . 5
β’
βπ₯ β
π βπ¦ β (π β {π₯}){π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))} β V |
5 | | eqid 2733 |
. . . . . 6
β’ (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) |
6 | 5 | fmpox 8000 |
. . . . 5
β’
(βπ₯ β
π βπ¦ β (π β {π₯}){π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))} β V β (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}):βͺ
π₯ β π ({π₯} Γ (π β {π₯}))βΆV) |
7 | 4, 6 | mpbi 229 |
. . . 4
β’ (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}):βͺ
π₯ β π ({π₯} Γ (π β {π₯}))βΆV |
8 | | ffn 6669 |
. . . 4
β’ ((π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}):βͺ
π₯ β π ({π₯} Γ (π β {π₯}))βΆV β (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) Fn βͺ
π₯ β π ({π₯} Γ (π β {π₯}))) |
9 | 7, 8 | ax-mp 5 |
. . 3
β’ (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) Fn βͺ
π₯ β π ({π₯} Γ (π β {π₯})) |
10 | | xpdifid 6121 |
. . . 4
β’ βͺ π₯ β π ({π₯} Γ (π β {π₯})) = ((π Γ π) β I ) |
11 | 10 | fneq2i 6601 |
. . 3
β’ ((π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) Fn βͺ
π₯ β π ({π₯} Γ (π β {π₯})) β (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) Fn ((π Γ π) β I )) |
12 | 9, 11 | mpbi 229 |
. 2
β’ (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) Fn ((π Γ π) β I ) |
13 | | tglng.l |
. . . 4
β’ πΏ = (LineGβπΊ) |
14 | | tglng.i |
. . . 4
β’ πΌ = (ItvβπΊ) |
15 | 1, 13, 14 | tglng 27530 |
. . 3
β’ (πΊ β TarskiG β πΏ = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))})) |
16 | 15 | fneq1d 6596 |
. 2
β’ (πΊ β TarskiG β (πΏ Fn ((π Γ π) β I ) β (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) Fn ((π Γ π) β I ))) |
17 | 12, 16 | mpbiri 258 |
1
β’ (πΊ β TarskiG β πΏ Fn ((π Γ π) β I )) |