Theorem swapf2fval

Description: The morphism part of the swap functor. See also swapf2fvala . (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Hypotheses	swapfval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
	swapfval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	swapf2fvala.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
	swapf2fvala.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	swapf2fvala.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝑆 ) )
	swapf2fval.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
Assertion	swapf2fval	⊢ ( 𝜑 → 𝑃 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		swapfval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
2		swapfval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3		swapf2fvala.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
4		swapf2fvala.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
5		swapf2fvala.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝑆 ) )
6		swapf2fval.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
7	6	fveq2d	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐶 swapF 𝐷 ) ) = ( 2nd ‘ ⟨ 𝑂 , 𝑃 ⟩ ) )
8	1 2 3 4 5	swapf2fvala	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐶 swapF 𝐷 ) ) = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) )
9	1 2	swapfelvv	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) ∈ ( V × V ) )
10	6 9	eqeltrrd	⊢ ( 𝜑 → ⟨ 𝑂 , 𝑃 ⟩ ∈ ( V × V ) )
11		opelxp	⊢ ( ⟨ 𝑂 , 𝑃 ⟩ ∈ ( V × V ) ↔ ( 𝑂 ∈ V ∧ 𝑃 ∈ V ) )
12	11	biimpi	⊢ ( ⟨ 𝑂 , 𝑃 ⟩ ∈ ( V × V ) → ( 𝑂 ∈ V ∧ 𝑃 ∈ V ) )
13		op2ndg	⊢ ( ( 𝑂 ∈ V ∧ 𝑃 ∈ V ) → ( 2nd ‘ ⟨ 𝑂 , 𝑃 ⟩ ) = 𝑃 )
14	10 12 13	3syl	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑂 , 𝑃 ⟩ ) = 𝑃 )
15	7 8 14	3eqtr3rd	⊢ ( 𝜑 → 𝑃 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) )