Step | Hyp | Ref
| Expression |
1 | | df-br 4584 |
. . 3
⊢ (𝐴(⟂G‘𝐺)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (⟂G‘𝐺)) |
2 | | df-perpg 25391 |
. . . . . 6
⊢ ⟂G
= (𝑔 ∈ V ↦
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔))}) |
3 | 2 | a1i 11 |
. . . . 5
⊢ (𝜑 → ⟂G = (𝑔 ∈ V ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔))})) |
4 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
5 | 4 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (LineG‘𝑔) = (LineG‘𝐺)) |
6 | | isperp.l |
. . . . . . . . . . 11
⊢ 𝐿 = (LineG‘𝐺) |
7 | 5, 6 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (LineG‘𝑔) = 𝐿) |
8 | 7 | rneqd 5274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → ran (LineG‘𝑔) = ran 𝐿) |
9 | 8 | eleq2d 2673 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (𝑎 ∈ ran (LineG‘𝑔) ↔ 𝑎 ∈ ran 𝐿)) |
10 | 8 | eleq2d 2673 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (𝑏 ∈ ran (LineG‘𝑔) ↔ 𝑏 ∈ ran 𝐿)) |
11 | 9, 10 | anbi12d 743 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ↔ (𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿))) |
12 | 4 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (∟G‘𝑔) = (∟G‘𝐺)) |
13 | 12 | eleq2d 2673 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔) ↔ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) |
14 | 13 | ralbidv 2969 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔) ↔ ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) |
15 | 14 | rexralbidv 3040 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔) ↔ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) |
16 | 11, 15 | anbi12d 743 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔)) ↔ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)))) |
17 | 16 | opabbidv 4648 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))}) |
18 | | isperp.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
19 | | elex 3185 |
. . . . . 6
⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ V) |
21 | | fvex 6113 |
. . . . . . . . 9
⊢
(LineG‘𝐺)
∈ V |
22 | 6, 21 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝐿 ∈ V |
23 | | rnexg 6990 |
. . . . . . . 8
⊢ (𝐿 ∈ V → ran 𝐿 ∈ V) |
24 | 22, 23 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ran 𝐿 ∈ V) |
25 | | xpexg 6858 |
. . . . . . 7
⊢ ((ran
𝐿 ∈ V ∧ ran 𝐿 ∈ V) → (ran 𝐿 × ran 𝐿) ∈ V) |
26 | 24, 24, 25 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (ran 𝐿 × ran 𝐿) ∈ V) |
27 | | opabssxp 5116 |
. . . . . . 7
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))} ⊆ (ran 𝐿 × ran 𝐿) |
28 | 27 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))} ⊆ (ran 𝐿 × ran 𝐿)) |
29 | 26, 28 | ssexd 4733 |
. . . . 5
⊢ (𝜑 → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))} ∈ V) |
30 | 3, 17, 20, 29 | fvmptd 6197 |
. . . 4
⊢ (𝜑 → (⟂G‘𝐺) = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))}) |
31 | 30 | eleq2d 2673 |
. . 3
⊢ (𝜑 → (〈𝐴, 𝐵〉 ∈ (⟂G‘𝐺) ↔ 〈𝐴, 𝐵〉 ∈ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))})) |
32 | 1, 31 | syl5bb 271 |
. 2
⊢ (𝜑 → (𝐴(⟂G‘𝐺)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))})) |
33 | | isperp.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ ran 𝐿) |
34 | | isperp.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ran 𝐿) |
35 | | ineq12 3771 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 ∩ 𝑏) = (𝐴 ∩ 𝐵)) |
36 | | simpll 786 |
. . . . . 6
⊢ (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ 𝑥 ∈ (𝑎 ∩ 𝑏)) → 𝑎 = 𝐴) |
37 | | simpllr 795 |
. . . . . . 7
⊢ ((((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ 𝑥 ∈ (𝑎 ∩ 𝑏)) ∧ 𝑢 ∈ 𝑎) → 𝑏 = 𝐵) |
38 | 37 | raleqdv 3121 |
. . . . . 6
⊢ ((((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ 𝑥 ∈ (𝑎 ∩ 𝑏)) ∧ 𝑢 ∈ 𝑎) → (∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺) ↔ ∀𝑣 ∈ 𝐵 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) |
39 | 36, 38 | raleqbidva 3131 |
. . . . 5
⊢ (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ 𝑥 ∈ (𝑎 ∩ 𝑏)) → (∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) |
40 | 35, 39 | rexeqbidva 3132 |
. . . 4
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺) ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐵)∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) |
41 | 40 | opelopab2a 4915 |
. . 3
⊢ ((𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿) → (〈𝐴, 𝐵〉 ∈ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))} ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐵)∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) |
42 | 33, 34, 41 | syl2anc 691 |
. 2
⊢ (𝜑 → (〈𝐴, 𝐵〉 ∈ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))} ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐵)∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) |
43 | 32, 42 | bitrd 267 |
1
⊢ (𝜑 → (𝐴(⟂G‘𝐺)𝐵 ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐵)∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) |