Theorem swapf1f1o

Description: The object part of the swap functor is a bijection between base sets. (Contributed by Zhi Wang, 8-Oct-2025)

	Ref	Expression
Hypotheses	swapf1f1o.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	swapf1f1o.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
	swapf1f1o.t	⊢ 𝑇 = ( 𝐷 ×c 𝐶 )
	swapf1f1o.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
	swapf1f1o.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	swapf1f1o.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	swapf1f1o.a	⊢ 𝐴 = ( Base ‘ 𝑇 )
Assertion	swapf1f1o	⊢ ( 𝜑 → 𝑂 : 𝐵 –1-1-onto→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		swapf1f1o.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		swapf1f1o.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
3		swapf1f1o.t	⊢ 𝑇 = ( 𝐷 ×c 𝐶 )
4		swapf1f1o.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
5		swapf1f1o.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
6		swapf1f1o.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
7		swapf1f1o.a	⊢ 𝐴 = ( Base ‘ 𝑇 )
8		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
10	2 8 9	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝑆 )
11	6 10	eqtr4i	⊢ 𝐵 = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) )
12	11	mpteq1i	⊢ ( 𝑥 ∈ 𝐵 ↦ ∪ ◡ { 𝑥 } ) = ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ∪ ◡ { 𝑥 } )
13	12	xpcomf1o	⊢ ( 𝑥 ∈ 𝐵 ↦ ∪ ◡ { 𝑥 } ) : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) –1-1-onto→ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐶 ) )
14	4 5 2 6 1	swapf1val	⊢ ( 𝜑 → 𝑂 = ( 𝑥 ∈ 𝐵 ↦ ∪ ◡ { 𝑥 } ) )
15	11	a1i	⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
16	3 9 8	xpcbas	⊢ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐶 ) ) = ( Base ‘ 𝑇 )
17	7 16	eqtr4i	⊢ 𝐴 = ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐶 ) )
18	17	a1i	⊢ ( 𝜑 → 𝐴 = ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐶 ) ) )
19	14 15 18	f1oeq123d	⊢ ( 𝜑 → ( 𝑂 : 𝐵 –1-1-onto→ 𝐴 ↔ ( 𝑥 ∈ 𝐵 ↦ ∪ ◡ { 𝑥 } ) : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) –1-1-onto→ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐶 ) ) ) )
20	13 19	mpbiri	⊢ ( 𝜑 → 𝑂 : 𝐵 –1-1-onto→ 𝐴 )