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