MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfiso2 Structured version   Visualization version   GIF version

Theorem dfiso2 17484
Description: Alternate definition of an isomorphism of a category, according to definition 3.8 in [Adamek] p. 28. (Contributed by AV, 10-Apr-2020.)
Hypotheses
Ref Expression
dfiso2.b 𝐵 = (Base‘𝐶)
dfiso2.h 𝐻 = (Hom ‘𝐶)
dfiso2.c (𝜑𝐶 ∈ Cat)
dfiso2.i 𝐼 = (Iso‘𝐶)
dfiso2.x (𝜑𝑋𝐵)
dfiso2.y (𝜑𝑌𝐵)
dfiso2.f (𝜑𝐹 ∈ (𝑋𝐻𝑌))
dfiso2.1 1 = (Id‘𝐶)
dfiso2.o = (⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)
dfiso2.p = (⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)
Assertion
Ref Expression
dfiso2 (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)((𝑔 𝐹) = ( 1𝑋) ∧ (𝐹 𝑔) = ( 1𝑌))))
Distinct variable groups:   𝐶,𝑔   𝑔,𝐹   𝑔,𝐻   𝑔,𝐼   𝑔,𝑋   𝑔,𝑌   ,𝑔   ,𝑔   1 ,𝑔   𝜑,𝑔
Allowed substitution hint:   𝐵(𝑔)

Proof of Theorem dfiso2
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef 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‘𝐶)
71, 2, 3, 4, 5, 6isoval 17477 . . 3 (𝜑 → (𝑋𝐼𝑌) = dom (𝑋(Inv‘𝐶)𝑌))
87eleq2d 2824 . 2 (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌)))
9 eqid 2738 . . . . 5 (Sect‘𝐶) = (Sect‘𝐶)
101, 2, 3, 4, 5, 9invfval 17471 . . . 4 (𝜑 → (𝑋(Inv‘𝐶)𝑌) = ((𝑋(Sect‘𝐶)𝑌) ∩ (𝑌(Sect‘𝐶)𝑋)))
1110dmeqd 5814 . . 3 (𝜑 → dom (𝑋(Inv‘𝐶)𝑌) = dom ((𝑋(Sect‘𝐶)𝑌) ∩ (𝑌(Sect‘𝐶)𝑋)))
1211eleq2d 2824 . 2 (𝜑 → (𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌) ↔ 𝐹 ∈ dom ((𝑋(Sect‘𝐶)𝑌) ∩ (𝑌(Sect‘𝐶)𝑋))))
13 dfiso2.h . . . . . . . . 9 𝐻 = (Hom ‘𝐶)
14 eqid 2738 . . . . . . . . 9 (comp‘𝐶) = (comp‘𝐶)
15 dfiso2.1 . . . . . . . . 9 1 = (Id‘𝐶)
161, 13, 14, 15, 9, 3, 4, 5sectfval 17463 . . . . . . . 8 (𝜑 → (𝑋(Sect‘𝐶)𝑌) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋))})
171, 13, 14, 15, 9, 3, 5, 4sectfval 17463 . . . . . . . . . 10 (𝜑 → (𝑌(Sect‘𝐶)𝑋) = {⟨𝑔, 𝑓⟩ ∣ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))})
1817cnveqd 5784 . . . . . . . . 9 (𝜑(𝑌(Sect‘𝐶)𝑋) = {⟨𝑔, 𝑓⟩ ∣ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))})
19 cnvopab 6042 . . . . . . . . 9 {⟨𝑔, 𝑓⟩ ∣ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))} = {⟨𝑓, 𝑔⟩ ∣ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))}
2018, 19eqtrdi 2794 . . . . . . . 8 (𝜑(𝑌(Sect‘𝐶)𝑋) = {⟨𝑓, 𝑔⟩ ∣ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))})
2116, 20ineq12d 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 (((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋))) ↔ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)))
2624, 25bitri 274 . . . . . . . . . . 11 (((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌))) ↔ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)))
2726anbi1i 624 . . . . . . . . . 10 ((((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌))) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))) ↔ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))))
2823, 27bitri 274 . . . . . . . . 9 ((((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋)) ∧ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))) ↔ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))))
2928opabbii 5141 . . . . . . . 8 {⟨𝑓, 𝑔⟩ ∣ (((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋)) ∧ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))}
3022, 29eqtri 2766 . . . . . . 7 ({⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋))} ∩ {⟨𝑓, 𝑔⟩ ∣ ((𝑔 ∈ (𝑌𝐻𝑋) ∧ 𝑓 ∈ (𝑋𝐻𝑌)) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))}) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))}
3121, 30eqtrdi 2794 . . . . . 6 (𝜑 → ((𝑋(Sect‘𝐶)𝑌) ∩ (𝑌(Sect‘𝐶)𝑋)) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))})
3231dmeqd 5814 . . . . 5 (𝜑 → dom ((𝑋(Sect‘𝐶)𝑌) ∩ (𝑌(Sect‘𝐶)𝑋)) = dom {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))})
33 dmopab 5824 . . . . 5 dom {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))} = {𝑓 ∣ ∃𝑔((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))}
3432, 33eqtrdi 2794 . . . 4 (𝜑 → dom ((𝑋(Sect‘𝐶)𝑌) ∩ (𝑌(Sect‘𝐶)𝑋)) = {𝑓 ∣ ∃𝑔((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))})
3534eleq2d 2824 . . 3 (𝜑 → (𝐹 ∈ dom ((𝑋(Sect‘𝐶)𝑌) ∩ (𝑌(Sect‘𝐶)𝑋)) ↔ 𝐹 ∈ {𝑓 ∣ ∃𝑔((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))}))
36 dfiso2.f . . . 4 (𝜑𝐹 ∈ (𝑋𝐻𝑌))
37 eleq1 2826 . . . . . . . 8 (𝑓 = 𝐹 → (𝑓 ∈ (𝑋𝐻𝑌) ↔ 𝐹 ∈ (𝑋𝐻𝑌)))
3837anbi1d 630 . . . . . . 7 (𝑓 = 𝐹 → ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋))))
39 oveq2 7283 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = (𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹))
4039eqeq1d 2740 . . . . . . . 8 (𝑓 = 𝐹 → ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ↔ (𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ( 1𝑋)))
41 oveq1 7282 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔))
4241eqeq1d 2740 . . . . . . . 8 (𝑓 = 𝐹 → ((𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌) ↔ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))
4340, 42anbi12d 631 . . . . . . 7 (𝑓 = 𝐹 → (((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)) ↔ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ( 1𝑋) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))))
4438, 43anbi12d 631 . . . . . 6 (𝑓 = 𝐹 → (((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))) ↔ ((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ( 1𝑋) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))))
4544exbidv 1924 . . . . 5 (𝑓 = 𝐹 → (∃𝑔((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))) ↔ ∃𝑔((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ( 1𝑋) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))))
4645elabg 3607 . . . 4 (𝐹 ∈ (𝑋𝐻𝑌) → (𝐹 ∈ {𝑓 ∣ ∃𝑔((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))} ↔ ∃𝑔((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ( 1𝑋) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))))
4736, 46syl 17 . . 3 (𝜑 → (𝐹 ∈ {𝑓 ∣ ∃𝑔((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝑓) = ( 1𝑋) ∧ (𝑓(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))} ↔ ∃𝑔((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ( 1𝑋) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)))))
4836biantrurd 533 . . . . . . 7 (𝜑 → (𝑔 ∈ (𝑌𝐻𝑋) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋))))
4948bicomd 222 . . . . . 6 (𝜑 → ((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ↔ 𝑔 ∈ (𝑌𝐻𝑋)))
50 dfiso2.o . . . . . . . . . . 11 = (⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)
5150a1i 11 . . . . . . . . . 10 (𝜑 = (⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋))
5251eqcomd 2744 . . . . . . . . 9 (𝜑 → (⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋) = )
5352oveqd 7292 . . . . . . . 8 (𝜑 → (𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = (𝑔 𝐹))
5453eqeq1d 2740 . . . . . . 7 (𝜑 → ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ( 1𝑋) ↔ (𝑔 𝐹) = ( 1𝑋)))
55 dfiso2.p . . . . . . . . . . 11 = (⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)
5655a1i 11 . . . . . . . . . 10 (𝜑 = (⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌))
5756eqcomd 2744 . . . . . . . . 9 (𝜑 → (⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌) = )
5857oveqd 7292 . . . . . . . 8 (𝜑 → (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = (𝐹 𝑔))
5958eqeq1d 2740 . . . . . . 7 (𝜑 → ((𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌) ↔ (𝐹 𝑔) = ( 1𝑌)))
6054, 59anbi12d 631 . . . . . 6 (𝜑 → (((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ( 1𝑋) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌)) ↔ ((𝑔 𝐹) = ( 1𝑋) ∧ (𝐹 𝑔) = ( 1𝑌))))
6149, 60anbi12d 631 . . . . 5 (𝜑 → (((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ( 1𝑋) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))) ↔ (𝑔 ∈ (𝑌𝐻𝑋) ∧ ((𝑔 𝐹) = ( 1𝑋) ∧ (𝐹 𝑔) = ( 1𝑌)))))
6261exbidv 1924 . . . 4 (𝜑 → (∃𝑔((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ( 1𝑋) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))) ↔ ∃𝑔(𝑔 ∈ (𝑌𝐻𝑋) ∧ ((𝑔 𝐹) = ( 1𝑋) ∧ (𝐹 𝑔) = ( 1𝑌)))))
63 df-rex 3070 . . . 4 (∃𝑔 ∈ (𝑌𝐻𝑋)((𝑔 𝐹) = ( 1𝑋) ∧ (𝐹 𝑔) = ( 1𝑌)) ↔ ∃𝑔(𝑔 ∈ (𝑌𝐻𝑋) ∧ ((𝑔 𝐹) = ( 1𝑋) ∧ (𝐹 𝑔) = ( 1𝑌))))
6462, 63bitr4di 289 . . 3 (𝜑 → (∃𝑔((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ( 1𝑋) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ( 1𝑌))) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)((𝑔 𝐹) = ( 1𝑋) ∧ (𝐹 𝑔) = ( 1𝑌))))
6535, 47, 643bitrd 305 . 2 (𝜑 → (𝐹 ∈ dom ((𝑋(Sect‘𝐶)𝑌) ∩ (𝑌(Sect‘𝐶)𝑋)) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)((𝑔 𝐹) = ( 1𝑋) ∧ (𝐹 𝑔) = ( 1𝑌))))
668, 12, 653bitrd 305 1 (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)((𝑔 𝐹) = ( 1𝑋) ∧ (𝐹 𝑔) = ( 1𝑌))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1539  wex 1782  wcel 2106  {cab 2715  wrex 3065  cin 3886  cop 4567  {copab 5136  ccnv 5588  dom cdm 5589  cfv 6433  (class class class)co 7275  Basecbs 16912  Hom chom 16973  compcco 16974  Catccat 17373  Idccid 17374  Sectcsect 17456  Invcinv 17457  Isociso 17458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832  df-sect 17459  df-inv 17460  df-iso 17461
This theorem is referenced by:  dfiso3  17485
  Copyright terms: Public domain W3C validator