Theorem swapf1vala

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

	Ref	Expression
Hypotheses	swapfval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
	swapfval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	swapf2fvala.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
	swapf2fvala.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion	swapf1vala	⊢ ( 𝜑 → ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) = ( 𝑥 ∈ 𝐵 ↦ ∪ ◡ { 𝑥 } ) )

Proof

Step	Hyp	Ref	Expression
1		swapfval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
2		swapfval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3		swapf2fvala.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
4		swapf2fvala.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
5		eqidd	⊢ ( 𝜑 → ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 ) )
6	1 2 3 4 5	swapfval	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ ( 𝑥 ∈ 𝐵 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑆 ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ )
7	6	fveq2d	⊢ ( 𝜑 → ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) = ( 1st ‘ ⟨ ( 𝑥 ∈ 𝐵 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑆 ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ ) )
8	4	fvexi	⊢ 𝐵 ∈ V
9	8	mptex	⊢ ( 𝑥 ∈ 𝐵 ↦ ∪ ◡ { 𝑥 } ) ∈ V
10	8 8	mpoex	⊢ ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑆 ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ∈ V
11	9 10	op1st	⊢ ( 1st ‘ ⟨ ( 𝑥 ∈ 𝐵 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑆 ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ ) = ( 𝑥 ∈ 𝐵 ↦ ∪ ◡ { 𝑥 } )
12	7 11	eqtrdi	⊢ ( 𝜑 → ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) = ( 𝑥 ∈ 𝐵 ↦ ∪ ◡ { 𝑥 } ) )