Step | Hyp | Ref
| Expression |
1 | | df-perpg 28440 |
. . . . . 6
β’ βG
= (π β V β¦
{β¨π, πβ© β£ ((π β ran (LineGβπ) β§ π β ran (LineGβπ)) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπ))}) |
2 | | simpr 484 |
. . . . . . . . . . . . 13
β’ ((π β§ π = πΊ) β π = πΊ) |
3 | 2 | fveq2d 6886 |
. . . . . . . . . . . 12
β’ ((π β§ π = πΊ) β (LineGβπ) = (LineGβπΊ)) |
4 | | perpln.l |
. . . . . . . . . . . 12
β’ πΏ = (LineGβπΊ) |
5 | 3, 4 | eqtr4di 2782 |
. . . . . . . . . . 11
β’ ((π β§ π = πΊ) β (LineGβπ) = πΏ) |
6 | 5 | rneqd 5928 |
. . . . . . . . . 10
β’ ((π β§ π = πΊ) β ran (LineGβπ) = ran πΏ) |
7 | 6 | eleq2d 2811 |
. . . . . . . . 9
β’ ((π β§ π = πΊ) β (π β ran (LineGβπ) β π β ran πΏ)) |
8 | 6 | eleq2d 2811 |
. . . . . . . . 9
β’ ((π β§ π = πΊ) β (π β ran (LineGβπ) β π β ran πΏ)) |
9 | 7, 8 | anbi12d 630 |
. . . . . . . 8
β’ ((π β§ π = πΊ) β ((π β ran (LineGβπ) β§ π β ran (LineGβπ)) β (π β ran πΏ β§ π β ran πΏ))) |
10 | 2 | fveq2d 6886 |
. . . . . . . . . . 11
β’ ((π β§ π = πΊ) β (βGβπ) = (βGβπΊ)) |
11 | 10 | eleq2d 2811 |
. . . . . . . . . 10
β’ ((π β§ π = πΊ) β (β¨βπ’π₯π£ββ© β (βGβπ) β β¨βπ’π₯π£ββ© β (βGβπΊ))) |
12 | 11 | ralbidv 3169 |
. . . . . . . . 9
β’ ((π β§ π = πΊ) β (βπ£ β π β¨βπ’π₯π£ββ© β (βGβπ) β βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))) |
13 | 12 | rexralbidv 3212 |
. . . . . . . 8
β’ ((π β§ π = πΊ) β (βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπ) β βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))) |
14 | 9, 13 | anbi12d 630 |
. . . . . . 7
β’ ((π β§ π = πΊ) β (((π β ran (LineGβπ) β§ π β ran (LineGβπ)) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπ)) β ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ)))) |
15 | 14 | opabbidv 5205 |
. . . . . 6
β’ ((π β§ π = πΊ) β {β¨π, πβ© β£ ((π β ran (LineGβπ) β§ π β ran (LineGβπ)) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπ))} = {β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))}) |
16 | | perpln.1 |
. . . . . . 7
β’ (π β πΊ β TarskiG) |
17 | 16 | elexd 3487 |
. . . . . 6
β’ (π β πΊ β V) |
18 | 4 | fvexi 6896 |
. . . . . . . . 9
β’ πΏ β V |
19 | | rnexg 7889 |
. . . . . . . . 9
β’ (πΏ β V β ran πΏ β V) |
20 | 18, 19 | mp1i 13 |
. . . . . . . 8
β’ (π β ran πΏ β V) |
21 | 20, 20 | xpexd 7732 |
. . . . . . 7
β’ (π β (ran πΏ Γ ran πΏ) β V) |
22 | | opabssxp 5759 |
. . . . . . . 8
β’
{β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))} β (ran πΏ Γ ran πΏ) |
23 | 22 | a1i 11 |
. . . . . . 7
β’ (π β {β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))} β (ran πΏ Γ ran πΏ)) |
24 | 21, 23 | ssexd 5315 |
. . . . . 6
β’ (π β {β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))} β V) |
25 | 1, 15, 17, 24 | fvmptd2 6997 |
. . . . 5
β’ (π β (βGβπΊ) = {β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))}) |
26 | | anass 468 |
. . . . . 6
β’ (((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ)) β (π β ran πΏ β§ (π β ran πΏ β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ)))) |
27 | 26 | opabbii 5206 |
. . . . 5
β’
{β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))} = {β¨π, πβ© β£ (π β ran πΏ β§ (π β ran πΏ β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ)))} |
28 | 25, 27 | eqtrdi 2780 |
. . . 4
β’ (π β (βGβπΊ) = {β¨π, πβ© β£ (π β ran πΏ β§ (π β ran πΏ β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ)))}) |
29 | 28 | dmeqd 5896 |
. . 3
β’ (π β dom (βGβπΊ) = dom {β¨π, πβ© β£ (π β ran πΏ β§ (π β ran πΏ β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ)))}) |
30 | | dmopabss 5909 |
. . 3
β’ dom
{β¨π, πβ© β£ (π β ran πΏ β§ (π β ran πΏ β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ)))} β ran πΏ |
31 | 29, 30 | eqsstrdi 4029 |
. 2
β’ (π β dom (βGβπΊ) β ran πΏ) |
32 | | relopabv 5812 |
. . . . . 6
β’ Rel
{β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))} |
33 | 25 | releqd 5769 |
. . . . . 6
β’ (π β (Rel
(βGβπΊ) β
Rel {β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))})) |
34 | 32, 33 | mpbiri 258 |
. . . . 5
β’ (π β Rel (βGβπΊ)) |
35 | | perpln.2 |
. . . . 5
β’ (π β π΄(βGβπΊ)π΅) |
36 | | brrelex12 5719 |
. . . . 5
β’ ((Rel
(βGβπΊ) β§
π΄(βGβπΊ)π΅) β (π΄ β V β§ π΅ β V)) |
37 | 34, 35, 36 | syl2anc 583 |
. . . 4
β’ (π β (π΄ β V β§ π΅ β V)) |
38 | 37 | simpld 494 |
. . 3
β’ (π β π΄ β V) |
39 | 37 | simprd 495 |
. . 3
β’ (π β π΅ β V) |
40 | | breldmg 5900 |
. . 3
β’ ((π΄ β V β§ π΅ β V β§ π΄(βGβπΊ)π΅) β π΄ β dom (βGβπΊ)) |
41 | 38, 39, 35, 40 | syl3anc 1368 |
. 2
β’ (π β π΄ β dom (βGβπΊ)) |
42 | 31, 41 | sseldd 3976 |
1
β’ (π β π΄ β ran πΏ) |