| Step | Hyp | Ref
| Expression |
| 1 | | lmif.m |
. . . . 5
⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) |
| 2 | | df-lmi 28783 |
. . . . . . 7
⊢ lInvG =
(𝑔 ∈ V ↦ (𝑑 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))))) |
| 3 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (LineG‘𝑔) = (LineG‘𝐺)) |
| 4 | | lmif.l |
. . . . . . . . . 10
⊢ 𝐿 = (LineG‘𝐺) |
| 5 | 3, 4 | eqtr4di 2795 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (LineG‘𝑔) = 𝐿) |
| 6 | 5 | rneqd 5949 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ran (LineG‘𝑔) = ran 𝐿) |
| 7 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
| 8 | | ismid.p |
. . . . . . . . . 10
⊢ 𝑃 = (Base‘𝐺) |
| 9 | 7, 8 | eqtr4di 2795 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃) |
| 10 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (midG‘𝑔) = (midG‘𝐺)) |
| 11 | 10 | oveqd 7448 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (𝑎(midG‘𝑔)𝑏) = (𝑎(midG‘𝐺)𝑏)) |
| 12 | 11 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ((𝑎(midG‘𝑔)𝑏) ∈ 𝑑 ↔ (𝑎(midG‘𝐺)𝑏) ∈ 𝑑)) |
| 13 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → 𝑑 = 𝑑) |
| 14 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (⟂G‘𝑔) = (⟂G‘𝐺)) |
| 15 | 5 | oveqd 7448 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (𝑎(LineG‘𝑔)𝑏) = (𝑎𝐿𝑏)) |
| 16 | 13, 14, 15 | breq123d 5157 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ↔ 𝑑(⟂G‘𝐺)(𝑎𝐿𝑏))) |
| 17 | 16 | orbi1d 917 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ((𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏) ↔ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))) |
| 18 | 12, 17 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (((𝑎(midG‘𝑔)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)) ↔ ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) |
| 19 | 9, 18 | riotaeqbidv 7391 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))) = (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) |
| 20 | 9, 19 | mpteq12dv 5233 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))) = (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) |
| 21 | 6, 20 | mpteq12dv 5233 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑑 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))) = (𝑑 ∈ ran 𝐿 ↦ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))))) |
| 22 | | ismid.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 23 | 22 | elexd 3504 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ V) |
| 24 | 4 | fvexi 6920 |
. . . . . . . . 9
⊢ 𝐿 ∈ V |
| 25 | | rnexg 7924 |
. . . . . . . . 9
⊢ (𝐿 ∈ V → ran 𝐿 ∈ V) |
| 26 | | mptexg 7241 |
. . . . . . . . 9
⊢ (ran
𝐿 ∈ V → (𝑑 ∈ ran 𝐿 ↦ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) ∈ V) |
| 27 | 24, 25, 26 | mp2b 10 |
. . . . . . . 8
⊢ (𝑑 ∈ ran 𝐿 ↦ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) ∈ V |
| 28 | 27 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑑 ∈ ran 𝐿 ↦ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) ∈ V) |
| 29 | 2, 21, 23, 28 | fvmptd3 7039 |
. . . . . 6
⊢ (𝜑 → (lInvG‘𝐺) = (𝑑 ∈ ran 𝐿 ↦ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))))) |
| 30 | | eleq2 2830 |
. . . . . . . . . 10
⊢ (𝑑 = 𝐷 → ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ↔ (𝑎(midG‘𝐺)𝑏) ∈ 𝐷)) |
| 31 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝐷 → (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ↔ 𝐷(⟂G‘𝐺)(𝑎𝐿𝑏))) |
| 32 | 31 | orbi1d 917 |
. . . . . . . . . 10
⊢ (𝑑 = 𝐷 → ((𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏) ↔ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))) |
| 33 | 30, 32 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → (((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)) ↔ ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) |
| 34 | 33 | riotabidv 7390 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))) = (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) |
| 35 | 34 | mpteq2dv 5244 |
. . . . . . 7
⊢ (𝑑 = 𝐷 → (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) = (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) |
| 36 | 35 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 = 𝐷) → (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝑑 ∧ (𝑑(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) = (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) |
| 37 | | lmif.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ ran 𝐿) |
| 38 | 8 | fvexi 6920 |
. . . . . . . 8
⊢ 𝑃 ∈ V |
| 39 | 38 | mptex 7243 |
. . . . . . 7
⊢ (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) ∈ V |
| 40 | 39 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)))) ∈ V) |
| 41 | 29, 36, 37, 40 | fvmptd 7023 |
. . . . 5
⊢ (𝜑 → ((lInvG‘𝐺)‘𝐷) = (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) |
| 42 | 1, 41 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → 𝑀 = (𝑎 ∈ 𝑃 ↦ (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))))) |
| 43 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑎(midG‘𝐺)𝑏) = (𝐴(midG‘𝐺)𝑏)) |
| 44 | 43 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ↔ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷)) |
| 45 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (𝑎𝐿𝑏) = (𝐴𝐿𝑏)) |
| 46 | 45 | breq2d 5155 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ↔ 𝐷(⟂G‘𝐺)(𝐴𝐿𝑏))) |
| 47 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑎 = 𝑏 ↔ 𝐴 = 𝑏)) |
| 48 | 46, 47 | orbi12d 919 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏) ↔ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) |
| 49 | 44, 48 | anbi12d 632 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)) ↔ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)))) |
| 50 | 49 | riotabidv 7390 |
. . . . 5
⊢ (𝑎 = 𝐴 → (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))) = (℩𝑏 ∈ 𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)))) |
| 51 | 50 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → (℩𝑏 ∈ 𝑃 ((𝑎(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))) = (℩𝑏 ∈ 𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)))) |
| 52 | | lmicl.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 53 | | ismid.d |
. . . . . 6
⊢ − =
(dist‘𝐺) |
| 54 | | ismid.i |
. . . . . 6
⊢ 𝐼 = (Itv‘𝐺) |
| 55 | | ismid.1 |
. . . . . 6
⊢ (𝜑 → 𝐺DimTarskiG≥2) |
| 56 | 8, 53, 54, 22, 55, 4, 37, 52 | lmieu 28792 |
. . . . 5
⊢ (𝜑 → ∃!𝑏 ∈ 𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) |
| 57 | | riotacl 7405 |
. . . . 5
⊢
(∃!𝑏 ∈
𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)) → (℩𝑏 ∈ 𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) ∈ 𝑃) |
| 58 | 56, 57 | syl 17 |
. . . 4
⊢ (𝜑 → (℩𝑏 ∈ 𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) ∈ 𝑃) |
| 59 | 42, 51, 52, 58 | fvmptd 7023 |
. . 3
⊢ (𝜑 → (𝑀‘𝐴) = (℩𝑏 ∈ 𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)))) |
| 60 | 59 | eqeq2d 2748 |
. 2
⊢ (𝜑 → (𝐵 = (𝑀‘𝐴) ↔ 𝐵 = (℩𝑏 ∈ 𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))))) |
| 61 | | islmib.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| 62 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (𝐴(midG‘𝐺)𝑏) = (𝐴(midG‘𝐺)𝐵)) |
| 63 | 62 | eleq1d 2826 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ↔ (𝐴(midG‘𝐺)𝐵) ∈ 𝐷)) |
| 64 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (𝐴𝐿𝑏) = (𝐴𝐿𝐵)) |
| 65 | 64 | breq2d 5155 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ↔ 𝐷(⟂G‘𝐺)(𝐴𝐿𝐵))) |
| 66 | | eqeq2 2749 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (𝐴 = 𝑏 ↔ 𝐴 = 𝐵)) |
| 67 | 65, 66 | orbi12d 919 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏) ↔ (𝐷(⟂G‘𝐺)(𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))) |
| 68 | 63, 67 | anbi12d 632 |
. . . . 5
⊢ (𝑏 = 𝐵 → (((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)) ↔ ((𝐴(midG‘𝐺)𝐵) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)))) |
| 69 | 68 | riota2 7413 |
. . . 4
⊢ ((𝐵 ∈ 𝑃 ∧ ∃!𝑏 ∈ 𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (((𝐴(midG‘𝐺)𝐵) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ↔ (℩𝑏 ∈ 𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) = 𝐵)) |
| 70 | 61, 56, 69 | syl2anc 584 |
. . 3
⊢ (𝜑 → (((𝐴(midG‘𝐺)𝐵) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ↔ (℩𝑏 ∈ 𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) = 𝐵)) |
| 71 | | eqcom 2744 |
. . 3
⊢ (𝐵 = (℩𝑏 ∈ 𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) ↔ (℩𝑏 ∈ 𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) = 𝐵) |
| 72 | 70, 71 | bitr4di 289 |
. 2
⊢ (𝜑 → (((𝐴(midG‘𝐺)𝐵) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ↔ 𝐵 = (℩𝑏 ∈ 𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))))) |
| 73 | 60, 72 | bitr4d 282 |
1
⊢ (𝜑 → (𝐵 = (𝑀‘𝐴) ↔ ((𝐴(midG‘𝐺)𝐵) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)))) |