Theorem dfswapf2

Description: Alternate definition of swapF ( df-swapf ). (Contributed by Zhi Wang, 9-Oct-2025)

	Ref	Expression
Assertion	dfswapf2	⊢ swapF = ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ⦋ ( 𝑐 ×c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		df-swapf	⊢ swapF = ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ⦋ ( 𝑐 ×c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ )
2		fvex	⊢ ( Base ‘ ( 𝑐 ×c 𝑑 ) ) ∈ V
3		id	⊢ ( 𝑏 = ( Base ‘ ( 𝑐 ×c 𝑑 ) ) → 𝑏 = ( Base ‘ ( 𝑐 ×c 𝑑 ) ) )
4		eqid	⊢ ( 𝑐 ×c 𝑑 ) = ( 𝑐 ×c 𝑑 )
5		eqid	⊢ ( Base ‘ 𝑐 ) = ( Base ‘ 𝑐 )
6		eqid	⊢ ( Base ‘ 𝑑 ) = ( Base ‘ 𝑑 )
7	4 5 6	xpcbas	⊢ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) = ( Base ‘ ( 𝑐 ×c 𝑑 ) )
8	3 7	eqtr4di	⊢ ( 𝑏 = ( Base ‘ ( 𝑐 ×c 𝑑 ) ) → 𝑏 = ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) )
9	8	mpteq1d	⊢ ( 𝑏 = ( Base ‘ ( 𝑐 ×c 𝑑 ) ) → ( 𝑥 ∈ 𝑏 ↦ ∪ ◡ { 𝑥 } ) = ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ∪ ◡ { 𝑥 } ) )
10		eqidd	⊢ ( 𝑏 = ( Base ‘ ( 𝑐 ×c 𝑑 ) ) → ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) = ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) )
11	8 8 10	mpoeq123dv	⊢ ( 𝑏 = ( Base ‘ ( 𝑐 ×c 𝑑 ) ) → ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) )
12	9 11	opeq12d	⊢ ( 𝑏 = ( Base ‘ ( 𝑐 ×c 𝑑 ) ) → ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ = ⟨ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ )
13	12	csbeq2dv	⊢ ( 𝑏 = ( Base ‘ ( 𝑐 ×c 𝑑 ) ) → ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ = ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ )
14	2 13	csbie	⊢ ⦋ ( Base ‘ ( 𝑐 ×c 𝑑 ) ) / 𝑏 ⦌ ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ = ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩
15		ovex	⊢ ( 𝑐 ×c 𝑑 ) ∈ V
16		fveq2	⊢ ( 𝑠 = ( 𝑐 ×c 𝑑 ) → ( Base ‘ 𝑠 ) = ( Base ‘ ( 𝑐 ×c 𝑑 ) ) )
17		fveq2	⊢ ( 𝑠 = ( 𝑐 ×c 𝑑 ) → ( Hom ‘ 𝑠 ) = ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) )
18	17	csbeq1d	⊢ ( 𝑠 = ( 𝑐 ×c 𝑑 ) → ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ = ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ )
19	16 18	csbeq12dv	⊢ ( 𝑠 = ( 𝑐 ×c 𝑑 ) → ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ = ⦋ ( Base ‘ ( 𝑐 ×c 𝑑 ) ) / 𝑏 ⦌ ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ )
20	15 19	csbie	⊢ ⦋ ( 𝑐 ×c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ = ⦋ ( Base ‘ ( 𝑐 ×c 𝑑 ) ) / 𝑏 ⦌ ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩
21	17	csbeq1d	⊢ ( 𝑠 = ( 𝑐 ×c 𝑑 ) → ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ = ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ )
22	16 21	csbeq12dv	⊢ ( 𝑠 = ( 𝑐 ×c 𝑑 ) → ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ = ⦋ ( Base ‘ ( 𝑐 ×c 𝑑 ) ) / 𝑏 ⦌ ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ )
23	15 22	csbie	⊢ ⦋ ( 𝑐 ×c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ = ⦋ ( Base ‘ ( 𝑐 ×c 𝑑 ) ) / 𝑏 ⦌ ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩
24	8	reseq2d	⊢ ( 𝑏 = ( Base ‘ ( 𝑐 ×c 𝑑 ) ) → ( tpos I ↾ 𝑏 ) = ( tpos I ↾ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) )
25		eqidd	⊢ ( 𝑏 = ( Base ‘ ( 𝑐 ×c 𝑑 ) ) → ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) = ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) )
26	8 8 25	mpoeq123dv	⊢ ( 𝑏 = ( Base ‘ ( 𝑐 ×c 𝑑 ) ) → ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) )
27	24 26	opeq12d	⊢ ( 𝑏 = ( Base ‘ ( 𝑐 ×c 𝑑 ) ) → ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ = ⟨ ( tpos I ↾ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ )
28	27	csbeq2dv	⊢ ( 𝑏 = ( Base ‘ ( 𝑐 ×c 𝑑 ) ) → ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ = ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( tpos I ↾ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ )
29	2 28	csbie	⊢ ⦋ ( Base ‘ ( 𝑐 ×c 𝑑 ) ) / 𝑏 ⦌ ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ = ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( tpos I ↾ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩
30		eqid	⊢ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) = ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) )
31	30	tposideq2	⊢ ( tpos I ↾ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) = ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ∪ ◡ { 𝑥 } )
32		eqid	⊢ ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝑐 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝑑 ) ( 2nd ‘ 𝑣 ) ) ) = ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝑐 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝑑 ) ( 2nd ‘ 𝑣 ) ) )
33	32	tposideq2	⊢ ( tpos I ↾ ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝑐 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝑑 ) ( 2nd ‘ 𝑣 ) ) ) ) = ( 𝑓 ∈ ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝑐 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝑑 ) ( 2nd ‘ 𝑣 ) ) ) ↦ ∪ ◡ { 𝑓 } )
34		eqid	⊢ ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝑐 )
35		eqid	⊢ ( Hom ‘ 𝑑 ) = ( Hom ‘ 𝑑 )
36		eqid	⊢ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) = ( Hom ‘ ( 𝑐 ×c 𝑑 ) )
37		simpl	⊢ ( ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) → 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) )
38		simpr	⊢ ( ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) → 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) )
39	4 7 34 35 36 37 38	xpchom	⊢ ( ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) → ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) = ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝑐 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝑑 ) ( 2nd ‘ 𝑣 ) ) ) )
40	39	reseq2d	⊢ ( ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) → ( tpos I ↾ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ) = ( tpos I ↾ ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝑐 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝑑 ) ( 2nd ‘ 𝑣 ) ) ) ) )
41	39	mpteq1d	⊢ ( ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) → ( 𝑓 ∈ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) = ( 𝑓 ∈ ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝑐 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝑑 ) ( 2nd ‘ 𝑣 ) ) ) ↦ ∪ ◡ { 𝑓 } ) )
42	33 40 41	3eqtr4a	⊢ ( ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) → ( tpos I ↾ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ) = ( 𝑓 ∈ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) )
43	42	mpoeq3ia	⊢ ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( tpos I ↾ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) )
44	31 43	opeq12i	⊢ ⟨ ( tpos I ↾ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( tpos I ↾ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ) ) ⟩ = ⟨ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩
45		fvex	⊢ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) ∈ V
46		oveq	⊢ ( ℎ = ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) → ( 𝑢 ℎ 𝑣 ) = ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) )
47	46	reseq2d	⊢ ( ℎ = ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) → ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) = ( tpos I ↾ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ) )
48	47	mpoeq3dv	⊢ ( ℎ = ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) → ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( tpos I ↾ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ) ) )
49	48	opeq2d	⊢ ( ℎ = ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) → ⟨ ( tpos I ↾ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ = ⟨ ( tpos I ↾ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( tpos I ↾ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ) ) ⟩ )
50	45 49	csbie	⊢ ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( tpos I ↾ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ = ⟨ ( tpos I ↾ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( tpos I ↾ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ) ) ⟩
51	46	mpteq1d	⊢ ( ℎ = ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) → ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) = ( 𝑓 ∈ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) )
52	51	mpoeq3dv	⊢ ( ℎ = ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) → ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) )
53	52	opeq2d	⊢ ( ℎ = ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) → ⟨ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ = ⟨ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ )
54	45 53	csbie	⊢ ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ = ⟨ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩
55	44 50 54	3eqtr4i	⊢ ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( tpos I ↾ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ = ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩
56	23 29 55	3eqtri	⊢ ⦋ ( 𝑐 ×c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ = ⦋ ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) / ℎ ⦌ ⟨ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩
57	14 20 56	3eqtr4ri	⊢ ⦋ ( 𝑐 ×c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ = ⦋ ( 𝑐 ×c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩
58	57	a1i	⊢ ( ( 𝑐 ∈ V ∧ 𝑑 ∈ V ) → ⦋ ( 𝑐 ×c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ = ⦋ ( 𝑐 ×c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ )
59	58	mpoeq3ia	⊢ ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ⦋ ( 𝑐 ×c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ ) = ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ⦋ ( 𝑐 ×c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) ⟩ )
60	1 59	eqtr4i	⊢ swapF = ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ⦋ ( 𝑐 ×c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( tpos I ↾ 𝑏 ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( tpos I ↾ ( 𝑢 ℎ 𝑣 ) ) ) ⟩ )