Metamath Proof Explorer

Theorem dfiso2

Description: Alternate definition of an isomorphism of a category, according to definition 3.8 in Adamek p. 28. (Contributed by AV, 10-Apr-2020)

Ref Expression
Hypotheses 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 dfiso2 ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ( ( 𝑔 ⚬ 𝐹 ) = ( 1 ‘ 𝑋 ) ∧ ( 𝐹 ∗ 𝑔 ) = ( 1 ‘ 𝑌 ) ) ) )

Proof

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