Metamath Proof Explorer


Theorem sectfval

Description: Value of the section relation. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses issect.b 𝐵 = ( Base ‘ 𝐶 )
issect.h 𝐻 = ( Hom ‘ 𝐶 )
issect.o · = ( comp ‘ 𝐶 )
issect.i 1 = ( Id ‘ 𝐶 )
issect.s 𝑆 = ( Sect ‘ 𝐶 )
issect.c ( 𝜑𝐶 ∈ Cat )
issect.x ( 𝜑𝑋𝐵 )
issect.y ( 𝜑𝑌𝐵 )
Assertion sectfval ( 𝜑 → ( 𝑋 𝑆 𝑌 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑋 ) 𝑓 ) = ( 1𝑋 ) ) } )

Proof

Step Hyp Ref Expression
1 issect.b 𝐵 = ( Base ‘ 𝐶 )
2 issect.h 𝐻 = ( Hom ‘ 𝐶 )
3 issect.o · = ( comp ‘ 𝐶 )
4 issect.i 1 = ( Id ‘ 𝐶 )
5 issect.s 𝑆 = ( Sect ‘ 𝐶 )
6 issect.c ( 𝜑𝐶 ∈ Cat )
7 issect.x ( 𝜑𝑋𝐵 )
8 issect.y ( 𝜑𝑌𝐵 )
9 1 2 3 4 5 6 7 7 sectffval ( 𝜑𝑆 = ( 𝑥𝐵 , 𝑦𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦· 𝑥 ) 𝑓 ) = ( 1𝑥 ) ) } ) )
10 simprl ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 )
11 simprr ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
12 10 11 oveq12d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
13 12 eleq2d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) )
14 11 10 oveq12d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑦 𝐻 𝑥 ) = ( 𝑌 𝐻 𝑋 ) )
15 14 eleq2d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ↔ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) )
16 13 15 anbi12d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ↔ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ) )
17 10 11 opeq12d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
18 17 10 oveq12d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( ⟨ 𝑥 , 𝑦· 𝑥 ) = ( ⟨ 𝑋 , 𝑌· 𝑋 ) )
19 18 oveqd ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦· 𝑥 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑋 ) 𝑓 ) )
20 10 fveq2d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 1𝑥 ) = ( 1𝑋 ) )
21 19 20 eqeq12d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦· 𝑥 ) 𝑓 ) = ( 1𝑥 ) ↔ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑋 ) 𝑓 ) = ( 1𝑋 ) ) )
22 16 21 anbi12d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦· 𝑥 ) 𝑓 ) = ( 1𝑥 ) ) ↔ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑋 ) 𝑓 ) = ( 1𝑋 ) ) ) )
23 22 opabbidv ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦· 𝑥 ) 𝑓 ) = ( 1𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑋 ) 𝑓 ) = ( 1𝑋 ) ) } )
24 ovex ( 𝑋 𝐻 𝑌 ) ∈ V
25 ovex ( 𝑌 𝐻 𝑋 ) ∈ V
26 24 25 xpex ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) ∈ V
27 opabssxp { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑋 ) 𝑓 ) = ( 1𝑋 ) ) } ⊆ ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) )
28 26 27 ssexi { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑋 ) 𝑓 ) = ( 1𝑋 ) ) } ∈ V
29 28 a1i ( 𝜑 → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑋 ) 𝑓 ) = ( 1𝑋 ) ) } ∈ V )
30 9 23 7 8 29 ovmpod ( 𝜑 → ( 𝑋 𝑆 𝑌 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑋 ) 𝑓 ) = ( 1𝑋 ) ) } )