Theorem swapf1

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

	Ref	Expression
Hypotheses	swapf1.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	swapf1.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
	swapf1.y	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
Assertion	swapf1	⊢ ( 𝜑 → ( 𝑋 𝑂 𝑌 ) = ⟨ 𝑌 , 𝑋 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		swapf1.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		swapf1.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
3		swapf1.y	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
4		df-ov	⊢ ( 𝑋 𝑂 𝑌 ) = ( 𝑂 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
5	2	elfvexd	⊢ ( 𝜑 → 𝐶 ∈ V )
6	3	elfvexd	⊢ ( 𝜑 → 𝐷 ∈ V )
7		eqid	⊢ ( 𝐶 ×c 𝐷 ) = ( 𝐶 ×c 𝐷 )
8		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
10	7 8 9	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ ( 𝐶 ×c 𝐷 ) )
11	5 6 7 10 1	swapf1val	⊢ ( 𝜑 → 𝑂 = ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ∪ ◡ { 𝑥 } ) )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ) → 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ )
13	12	sneqd	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ) → { 𝑥 } = { ⟨ 𝑋 , 𝑌 ⟩ } )
14	13	cnveqd	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ) → ◡ { 𝑥 } = ◡ { ⟨ 𝑋 , 𝑌 ⟩ } )
15	14	unieqd	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ) → ∪ ◡ { 𝑥 } = ∪ ◡ { ⟨ 𝑋 , 𝑌 ⟩ } )
16		opswap	⊢ ∪ ◡ { ⟨ 𝑋 , 𝑌 ⟩ } = ⟨ 𝑌 , 𝑋 ⟩
17	15 16	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ) → ∪ ◡ { 𝑥 } = ⟨ 𝑌 , 𝑋 ⟩ )
18	2 3	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
19		opex	⊢ ⟨ 𝑌 , 𝑋 ⟩ ∈ V
20	19	a1i	⊢ ( 𝜑 → ⟨ 𝑌 , 𝑋 ⟩ ∈ V )
21	11 17 18 20	fvmptd	⊢ ( 𝜑 → ( 𝑂 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ 𝑌 , 𝑋 ⟩ )
22	4 21	eqtrid	⊢ ( 𝜑 → ( 𝑋 𝑂 𝑌 ) = ⟨ 𝑌 , 𝑋 ⟩ )