Theorem swapf1a

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

	Ref	Expression
Hypotheses	swapf1a.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	swapf1a.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
	swapf1a.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	swapf1a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	swapf1a	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = ⟨ ( 2nd ‘ 𝑋 ) , ( 1st ‘ 𝑋 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		swapf1a.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		swapf1a.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
3		swapf1a.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
4		swapf1a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5	2 3 4	elxpcbasex1	⊢ ( 𝜑 → 𝐶 ∈ V )
6	2 3 4	elxpcbasex2	⊢ ( 𝜑 → 𝐷 ∈ V )
7	5 6 2 3 1	swapf1val	⊢ ( 𝜑 → 𝑂 = ( 𝑥 ∈ 𝐵 ↦ ∪ ◡ { 𝑥 } ) )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
9	8	sneqd	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → { 𝑥 } = { 𝑋 } )
10	9	cnveqd	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ◡ { 𝑥 } = ◡ { 𝑋 } )
11	10	unieqd	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ∪ ◡ { 𝑥 } = ∪ ◡ { 𝑋 } )
12		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
13		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
14	2 12 13	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝑆 )
15	3 14	eqtr4i	⊢ 𝐵 = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) )
16	4 15	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
17		2nd1st	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ∪ ◡ { 𝑋 } = ⟨ ( 2nd ‘ 𝑋 ) , ( 1st ‘ 𝑋 ) ⟩ )
18	16 17	syl	⊢ ( 𝜑 → ∪ ◡ { 𝑋 } = ⟨ ( 2nd ‘ 𝑋 ) , ( 1st ‘ 𝑋 ) ⟩ )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ∪ ◡ { 𝑋 } = ⟨ ( 2nd ‘ 𝑋 ) , ( 1st ‘ 𝑋 ) ⟩ )
20	11 19	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ∪ ◡ { 𝑥 } = ⟨ ( 2nd ‘ 𝑋 ) , ( 1st ‘ 𝑋 ) ⟩ )
21		opex	⊢ ⟨ ( 2nd ‘ 𝑋 ) , ( 1st ‘ 𝑋 ) ⟩ ∈ V
22	21	a1i	⊢ ( 𝜑 → ⟨ ( 2nd ‘ 𝑋 ) , ( 1st ‘ 𝑋 ) ⟩ ∈ V )
23	7 20 4 22	fvmptd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = ⟨ ( 2nd ‘ 𝑋 ) , ( 1st ‘ 𝑋 ) ⟩ )