Step | Hyp | Ref
| Expression |
1 | | df-perpg 26482 |
. . . . . 6
⊢ ⟂G
= (𝑔 ∈ V ↦
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔))}) |
2 | | simpr 487 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
3 | 2 | fveq2d 6674 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (LineG‘𝑔) = (LineG‘𝐺)) |
4 | | perpln.l |
. . . . . . . . . . . 12
⊢ 𝐿 = (LineG‘𝐺) |
5 | 3, 4 | syl6eqr 2874 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (LineG‘𝑔) = 𝐿) |
6 | 5 | rneqd 5808 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → ran (LineG‘𝑔) = ran 𝐿) |
7 | 6 | eleq2d 2898 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (𝑎 ∈ ran (LineG‘𝑔) ↔ 𝑎 ∈ ran 𝐿)) |
8 | 6 | eleq2d 2898 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (𝑏 ∈ ran (LineG‘𝑔) ↔ 𝑏 ∈ ran 𝐿)) |
9 | 7, 8 | anbi12d 632 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ↔ (𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿))) |
10 | 2 | fveq2d 6674 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (∟G‘𝑔) = (∟G‘𝐺)) |
11 | 10 | eleq2d 2898 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔) ↔ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) |
12 | 11 | ralbidv 3197 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔) ↔ ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) |
13 | 12 | rexralbidv 3301 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔) ↔ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) |
14 | 9, 13 | anbi12d 632 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔)) ↔ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)))) |
15 | 14 | opabbidv 5132 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))}) |
16 | | perpln.1 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
17 | 16 | elexd 3514 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ V) |
18 | 4 | fvexi 6684 |
. . . . . . . . 9
⊢ 𝐿 ∈ V |
19 | | rnexg 7614 |
. . . . . . . . 9
⊢ (𝐿 ∈ V → ran 𝐿 ∈ V) |
20 | 18, 19 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐿 ∈ V) |
21 | 20, 20 | xpexd 7474 |
. . . . . . 7
⊢ (𝜑 → (ran 𝐿 × ran 𝐿) ∈ V) |
22 | | opabssxp 5643 |
. . . . . . . 8
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))} ⊆ (ran 𝐿 × ran 𝐿) |
23 | 22 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))} ⊆ (ran 𝐿 × ran 𝐿)) |
24 | 21, 23 | ssexd 5228 |
. . . . . 6
⊢ (𝜑 → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))} ∈ V) |
25 | 1, 15, 17, 24 | fvmptd2 6776 |
. . . . 5
⊢ (𝜑 → (⟂G‘𝐺) = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))}) |
26 | | anass 471 |
. . . . . 6
⊢ (((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) ↔ (𝑎 ∈ ran 𝐿 ∧ (𝑏 ∈ ran 𝐿 ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)))) |
27 | 26 | opabbii 5133 |
. . . . 5
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))} = {〈𝑎, 𝑏〉 ∣ (𝑎 ∈ ran 𝐿 ∧ (𝑏 ∈ ran 𝐿 ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)))} |
28 | 25, 27 | syl6eq 2872 |
. . . 4
⊢ (𝜑 → (⟂G‘𝐺) = {〈𝑎, 𝑏〉 ∣ (𝑎 ∈ ran 𝐿 ∧ (𝑏 ∈ ran 𝐿 ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)))}) |
29 | 28 | dmeqd 5774 |
. . 3
⊢ (𝜑 → dom (⟂G‘𝐺) = dom {〈𝑎, 𝑏〉 ∣ (𝑎 ∈ ran 𝐿 ∧ (𝑏 ∈ ran 𝐿 ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)))}) |
30 | | dmopabss 5787 |
. . 3
⊢ dom
{〈𝑎, 𝑏〉 ∣ (𝑎 ∈ ran 𝐿 ∧ (𝑏 ∈ ran 𝐿 ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)))} ⊆ ran 𝐿 |
31 | 29, 30 | eqsstrdi 4021 |
. 2
⊢ (𝜑 → dom (⟂G‘𝐺) ⊆ ran 𝐿) |
32 | | relopab 5696 |
. . . . . 6
⊢ Rel
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))} |
33 | 25 | releqd 5653 |
. . . . . 6
⊢ (𝜑 → (Rel
(⟂G‘𝐺) ↔
Rel {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))})) |
34 | 32, 33 | mpbiri 260 |
. . . . 5
⊢ (𝜑 → Rel (⟂G‘𝐺)) |
35 | | perpln.2 |
. . . . 5
⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵) |
36 | | brrelex12 5604 |
. . . . 5
⊢ ((Rel
(⟂G‘𝐺) ∧
𝐴(⟂G‘𝐺)𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
37 | 34, 35, 36 | syl2anc 586 |
. . . 4
⊢ (𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
38 | 37 | simpld 497 |
. . 3
⊢ (𝜑 → 𝐴 ∈ V) |
39 | 37 | simprd 498 |
. . 3
⊢ (𝜑 → 𝐵 ∈ V) |
40 | | breldmg 5778 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴(⟂G‘𝐺)𝐵) → 𝐴 ∈ dom (⟂G‘𝐺)) |
41 | 38, 39, 35, 40 | syl3anc 1367 |
. 2
⊢ (𝜑 → 𝐴 ∈ dom (⟂G‘𝐺)) |
42 | 31, 41 | sseldd 3968 |
1
⊢ (𝜑 → 𝐴 ∈ ran 𝐿) |