Step | Hyp | Ref
| Expression |
1 | | dfiso2.b |
. . . 4
⊢ 𝐵 = (Base‘𝐶) |
2 | | eqid 2738 |
. . . 4
⊢
(Inv‘𝐶) =
(Inv‘𝐶) |
3 | | dfiso2.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
4 | | dfiso2.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
5 | | dfiso2.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
6 | | dfiso2.i |
. . . 4
⊢ 𝐼 = (Iso‘𝐶) |
7 | 1, 2, 3, 4, 5, 6 | isoval 17477 |
. . 3
⊢ (𝜑 → (𝑋𝐼𝑌) = dom (𝑋(Inv‘𝐶)𝑌)) |
8 | 7 | eleq2d 2824 |
. 2
⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌))) |
9 | | eqid 2738 |
. . . . 5
⊢
(Sect‘𝐶) =
(Sect‘𝐶) |
10 | 1, 2, 3, 4, 5, 9 | invfval 17471 |
. . . 4
⊢ (𝜑 → (𝑋(Inv‘𝐶)𝑌) = ((𝑋(Sect‘𝐶)𝑌) ∩ ◡(𝑌(Sect‘𝐶)𝑋))) |
11 | 10 | dmeqd 5814 |
. . 3
⊢ (𝜑 → dom (𝑋(Inv‘𝐶)𝑌) = dom ((𝑋(Sect‘𝐶)𝑌) ∩ ◡(𝑌(Sect‘𝐶)𝑋))) |
12 | 11 | eleq2d 2824 |
. 2
⊢ (𝜑 → (𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌) ↔ 𝐹 ∈ dom ((𝑋(Sect‘𝐶)𝑌) ∩ ◡(𝑌(Sect‘𝐶)𝑋)))) |
13 | | dfiso2.h |
. . . . . . . . 9
⊢ 𝐻 = (Hom ‘𝐶) |
14 | | eqid 2738 |
. . . . . . . . 9
⊢
(comp‘𝐶) =
(comp‘𝐶) |
15 | | dfiso2.1 |
. . . . . . . . 9
⊢ 1 =
(Id‘𝐶) |
16 | 1, 13, 14, 15, 9, 3, 4, 5 | sectfval 17463 |
. . . . . . . 8
⊢ (𝜑 → (𝑋(Sect‘𝐶)𝑌) = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋))}) |
17 | 1, 13, 14, 15, 9, 3, 5, 4 | sectfval 17463 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌(Sect‘𝐶)𝑋) = {〈𝑔, 𝑓〉 ∣ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))}) |
18 | 17 | cnveqd 5784 |
. . . . . . . . 9
⊢ (𝜑 → ◡(𝑌(Sect‘𝐶)𝑋) = ◡{〈𝑔, 𝑓〉 ∣ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))}) |
19 | | cnvopab 6042 |
. . . . . . . . 9
⊢ ◡{〈𝑔, 𝑓〉 ∣ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))} = {〈𝑓, 𝑔〉 ∣ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))} |
20 | 18, 19 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝜑 → ◡(𝑌(Sect‘𝐶)𝑋) = {〈𝑓, 𝑔〉 ∣ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))}) |
21 | 16, 20 | ineq12d 4147 |
. . . . . . 7
⊢ (𝜑 → ((𝑋(Sect‘𝐶)𝑌) ∩ ◡(𝑌(Sect‘𝐶)𝑋)) = ({〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋))} ∩ {〈𝑓, 𝑔〉 ∣ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))})) |
22 | | inopab 5739 |
. . . . . . . 8
⊢
({〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋))} ∩ {〈𝑓, 𝑔〉 ∣ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))}) = {〈𝑓, 𝑔〉 ∣ (((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋)) ∧ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))} |
23 | | an4 653 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋)) ∧ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))) ↔ (((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌))) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))) |
24 | | an42 654 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌))) ↔ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)))) |
25 | | anidm 565 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋))) ↔ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋))) |
26 | 24, 25 | bitri 274 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌))) ↔ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋))) |
27 | 26 | anbi1i 624 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌))) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))) ↔ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))) |
28 | 23, 27 | bitri 274 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋)) ∧ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))) ↔ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))) |
29 | 28 | opabbii 5141 |
. . . . . . . 8
⊢
{〈𝑓, 𝑔〉 ∣ (((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋)) ∧ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))} = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))} |
30 | 22, 29 | eqtri 2766 |
. . . . . . 7
⊢
({〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋))} ∩ {〈𝑓, 𝑔〉 ∣ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))}) = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))} |
31 | 21, 30 | eqtrdi 2794 |
. . . . . 6
⊢ (𝜑 → ((𝑋(Sect‘𝐶)𝑌) ∩ ◡(𝑌(Sect‘𝐶)𝑋)) = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))}) |
32 | 31 | dmeqd 5814 |
. . . . 5
⊢ (𝜑 → dom ((𝑋(Sect‘𝐶)𝑌) ∩ ◡(𝑌(Sect‘𝐶)𝑋)) = dom {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))}) |
33 | | dmopab 5824 |
. . . . 5
⊢ dom
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))} = {𝑓 ∣ ∃𝑔((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))} |
34 | 32, 33 | eqtrdi 2794 |
. . . 4
⊢ (𝜑 → dom ((𝑋(Sect‘𝐶)𝑌) ∩ ◡(𝑌(Sect‘𝐶)𝑋)) = {𝑓 ∣ ∃𝑔((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))}) |
35 | 34 | eleq2d 2824 |
. . 3
⊢ (𝜑 → (𝐹 ∈ dom ((𝑋(Sect‘𝐶)𝑌) ∩ ◡(𝑌(Sect‘𝐶)𝑋)) ↔ 𝐹 ∈ {𝑓 ∣ ∃𝑔((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))})) |
36 | | dfiso2.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) |
37 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑓 ∈ (𝑋𝐻𝑌) ↔ 𝐹 ∈ (𝑋𝐻𝑌))) |
38 | 37 | anbi1d 630 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)))) |
39 | | oveq2 7283 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹)) |
40 | 39 | eqeq1d 2740 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ↔ (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ( 1 ‘𝑋))) |
41 | | oveq1 7282 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔)) |
42 | 41 | eqeq1d 2740 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → ((𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌) ↔ (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))) |
43 | 40, 42 | anbi12d 631 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)) ↔ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ( 1 ‘𝑋) ∧ (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))) |
44 | 38, 43 | anbi12d 631 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))) ↔ ((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ( 1 ‘𝑋) ∧ (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))))) |
45 | 44 | exbidv 1924 |
. . . . 5
⊢ (𝑓 = 𝐹 → (∃𝑔((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))) ↔ ∃𝑔((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ( 1 ‘𝑋) ∧ (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))))) |
46 | 45 | elabg 3607 |
. . . 4
⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (𝐹 ∈ {𝑓 ∣ ∃𝑔((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))} ↔ ∃𝑔((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ( 1 ‘𝑋) ∧ (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))))) |
47 | 36, 46 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹 ∈ {𝑓 ∣ ∃𝑔((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝑓) = ( 1 ‘𝑋) ∧ (𝑓(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)))} ↔ ∃𝑔((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ( 1 ‘𝑋) ∧ (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))))) |
48 | 36 | biantrurd 533 |
. . . . . . 7
⊢ (𝜑 → (𝑔 ∈ (𝑌𝐻𝑋) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)))) |
49 | 48 | bicomd 222 |
. . . . . 6
⊢ (𝜑 → ((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ↔ 𝑔 ∈ (𝑌𝐻𝑋))) |
50 | | dfiso2.o |
. . . . . . . . . . 11
⊢ ⚬ =
(〈𝑋, 𝑌〉(comp‘𝐶)𝑋) |
51 | 50 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ⚬ = (〈𝑋, 𝑌〉(comp‘𝐶)𝑋)) |
52 | 51 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝜑 → (〈𝑋, 𝑌〉(comp‘𝐶)𝑋) = ⚬ ) |
53 | 52 | oveqd 7292 |
. . . . . . . 8
⊢ (𝜑 → (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = (𝑔 ⚬ 𝐹)) |
54 | 53 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝜑 → ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ( 1 ‘𝑋) ↔ (𝑔 ⚬ 𝐹) = ( 1 ‘𝑋))) |
55 | | dfiso2.p |
. . . . . . . . . . 11
⊢ ∗ =
(〈𝑌, 𝑋〉(comp‘𝐶)𝑌) |
56 | 55 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ∗ = (〈𝑌, 𝑋〉(comp‘𝐶)𝑌)) |
57 | 56 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝜑 → (〈𝑌, 𝑋〉(comp‘𝐶)𝑌) = ∗ ) |
58 | 57 | oveqd 7292 |
. . . . . . . 8
⊢ (𝜑 → (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹 ∗ 𝑔)) |
59 | 58 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝜑 → ((𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌) ↔ (𝐹 ∗ 𝑔) = ( 1 ‘𝑌))) |
60 | 54, 59 | anbi12d 631 |
. . . . . 6
⊢ (𝜑 → (((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ( 1 ‘𝑋) ∧ (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌)) ↔ ((𝑔 ⚬ 𝐹) = ( 1 ‘𝑋) ∧ (𝐹 ∗ 𝑔) = ( 1 ‘𝑌)))) |
61 | 49, 60 | anbi12d 631 |
. . . . 5
⊢ (𝜑 → (((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ( 1 ‘𝑋) ∧ (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))) ↔ (𝑔 ∈ (𝑌𝐻𝑋) ∧ ((𝑔 ⚬ 𝐹) = ( 1 ‘𝑋) ∧ (𝐹 ∗ 𝑔) = ( 1 ‘𝑌))))) |
62 | 61 | exbidv 1924 |
. . . 4
⊢ (𝜑 → (∃𝑔((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ( 1 ‘𝑋) ∧ (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))) ↔ ∃𝑔(𝑔 ∈ (𝑌𝐻𝑋) ∧ ((𝑔 ⚬ 𝐹) = ( 1 ‘𝑋) ∧ (𝐹 ∗ 𝑔) = ( 1 ‘𝑌))))) |
63 | | df-rex 3070 |
. . . 4
⊢
(∃𝑔 ∈
(𝑌𝐻𝑋)((𝑔 ⚬ 𝐹) = ( 1 ‘𝑋) ∧ (𝐹 ∗ 𝑔) = ( 1 ‘𝑌)) ↔ ∃𝑔(𝑔 ∈ (𝑌𝐻𝑋) ∧ ((𝑔 ⚬ 𝐹) = ( 1 ‘𝑋) ∧ (𝐹 ∗ 𝑔) = ( 1 ‘𝑌)))) |
64 | 62, 63 | bitr4di 289 |
. . 3
⊢ (𝜑 → (∃𝑔((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ( 1 ‘𝑋) ∧ (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝑔) = ( 1 ‘𝑌))) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)((𝑔 ⚬ 𝐹) = ( 1 ‘𝑋) ∧ (𝐹 ∗ 𝑔) = ( 1 ‘𝑌)))) |
65 | 35, 47, 64 | 3bitrd 305 |
. 2
⊢ (𝜑 → (𝐹 ∈ dom ((𝑋(Sect‘𝐶)𝑌) ∩ ◡(𝑌(Sect‘𝐶)𝑋)) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)((𝑔 ⚬ 𝐹) = ( 1 ‘𝑋) ∧ (𝐹 ∗ 𝑔) = ( 1 ‘𝑌)))) |
66 | 8, 12, 65 | 3bitrd 305 |
1
⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)((𝑔 ⚬ 𝐹) = ( 1 ‘𝑋) ∧ (𝐹 ∗ 𝑔) = ( 1 ‘𝑌)))) |