Step | Hyp | Ref
| Expression |
1 | | tglng.p |
. . . . . . . 8
β’ π = (BaseβπΊ) |
2 | | tglng.l |
. . . . . . . 8
β’ πΏ = (LineGβπΊ) |
3 | | tglng.i |
. . . . . . . 8
β’ πΌ = (ItvβπΊ) |
4 | 1, 2, 3 | tglng 27537 |
. . . . . . 7
β’ (πΊ β TarskiG β πΏ = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))})) |
5 | 4 | rneqd 5897 |
. . . . . 6
β’ (πΊ β TarskiG β ran πΏ = ran (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))})) |
6 | 5 | eleq2d 2820 |
. . . . 5
β’ (πΊ β TarskiG β (π β ran πΏ β π β ran (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}))) |
7 | 6 | biimpa 478 |
. . . 4
β’ ((πΊ β TarskiG β§ π β ran πΏ) β π β ran (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))})) |
8 | | eqid 2733 |
. . . . . 6
β’ (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) |
9 | 1 | fvexi 6860 |
. . . . . . 7
β’ π β V |
10 | 9 | rabex 5293 |
. . . . . 6
β’ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))} β V |
11 | 8, 10 | elrnmpo 7496 |
. . . . 5
β’ (π β ran (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) β βπ₯ β π βπ¦ β (π β {π₯})π = {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) |
12 | | ssrab2 4041 |
. . . . . . . 8
β’ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))} β π |
13 | | sseq1 3973 |
. . . . . . . 8
β’ (π = {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))} β (π β π β {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))} β π)) |
14 | 12, 13 | mpbiri 258 |
. . . . . . 7
β’ (π = {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))} β π β π) |
15 | 14 | rexlimivw 3145 |
. . . . . 6
β’
(βπ¦ β
(π β {π₯})π = {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))} β π β π) |
16 | 15 | rexlimivw 3145 |
. . . . 5
β’
(βπ₯ β
π βπ¦ β (π β {π₯})π = {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))} β π β π) |
17 | 11, 16 | sylbi 216 |
. . . 4
β’ (π β ran (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) β π β π) |
18 | 7, 17 | syl 17 |
. . 3
β’ ((πΊ β TarskiG β§ π β ran πΏ) β π β π) |
19 | 18 | ralrimiva 3140 |
. 2
β’ (πΊ β TarskiG β
βπ β ran πΏ π β π) |
20 | | unissb 4904 |
. 2
β’ (βͺ ran πΏ β π β βπ β ran πΏ π β π) |
21 | 19, 20 | sylibr 233 |
1
β’ (πΊ β TarskiG β βͺ ran πΏ β π) |