Theorem swapfelvv

Description: A swap functor is an ordered pair. (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Hypotheses	swapfval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
	swapfval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
Assertion	swapfelvv	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) ∈ ( V × V ) )

Proof

Step	Hyp	Ref	Expression
1		swapfval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
2		swapfval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3		eqid	⊢ ( 𝐶 ×c 𝐷 ) = ( 𝐶 ×c 𝐷 )
4		eqid	⊢ ( Base ‘ ( 𝐶 ×c 𝐷 ) ) = ( Base ‘ ( 𝐶 ×c 𝐷 ) )
5		eqidd	⊢ ( 𝜑 → ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) )
6	1 2 3 4 5	swapfval	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ ( 𝑥 ∈ ( Base ‘ ( 𝐶 ×c 𝐷 ) ) ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ ( Base ‘ ( 𝐶 ×c 𝐷 ) ) , 𝑣 ∈ ( Base ‘ ( 𝐶 ×c 𝐷 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ )
7		fvex	⊢ ( Base ‘ ( 𝐶 ×c 𝐷 ) ) ∈ V
8	7	mptex	⊢ ( 𝑥 ∈ ( Base ‘ ( 𝐶 ×c 𝐷 ) ) ↦ ∪ ◡ { 𝑥 } ) ∈ V
9	7 7	mpoex	⊢ ( 𝑢 ∈ ( Base ‘ ( 𝐶 ×c 𝐷 ) ) , 𝑣 ∈ ( Base ‘ ( 𝐶 ×c 𝐷 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ∈ V
10	8 9	opelvv	⊢ ⟨ ( 𝑥 ∈ ( Base ‘ ( 𝐶 ×c 𝐷 ) ) ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ ( Base ‘ ( 𝐶 ×c 𝐷 ) ) , 𝑣 ∈ ( Base ‘ ( 𝐶 ×c 𝐷 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ ∈ ( V × V )
11	6 10	eqeltrdi	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) ∈ ( V × V ) )