swapfval

Description: Value of the swap functor. (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Hypotheses	swapfval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
	swapfval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	swapfval.s	⊢ 𝑆 = ( 𝐶 ×_c 𝐷 )
	swapfval.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	swapfval.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝑆 ) )
Assertion	swapfval	⊢ ( 𝜑 → ( 𝐶 swap_F 𝐷 ) = ⟨ ( 𝑥 ∈ 𝐵 ↦ ∪ ^◡ { 𝑥 } ) , ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		swapfval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
2		swapfval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3		swapfval.s	⊢ 𝑆 = ( 𝐶 ×_c 𝐷 )
4		swapfval.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
5		swapfval.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝑆 ) )
6		df-swapf	⊢ swap_F = ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ⦋ ( 𝑐 ×_c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ^◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) ⟩ )
7	6	a1i	⊢ ( 𝜑 → swap_F = ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ⦋ ( 𝑐 ×_c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ^◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) ⟩ ) )
8		ovexd	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → ( 𝑐 ×_c 𝑑 ) ∈ V )
9		simprl	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → 𝑐 = 𝐶 )
10		simprr	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → 𝑑 = 𝐷 )
11	9 10	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → ( 𝑐 ×_c 𝑑 ) = ( 𝐶 ×_c 𝐷 ) )
12	11 3	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → ( 𝑐 ×_c 𝑑 ) = 𝑆 )
13		fvexd	⊢ ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) → ( Base ‘ 𝑠 ) ∈ V )
14		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 )
15	14	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
16	15 4	eqtr4di	⊢ ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) → ( Base ‘ 𝑠 ) = 𝐵 )
17		fvexd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑠 ) ∈ V )
18		simplr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = 𝐵 ) → 𝑠 = 𝑆 )
19	18	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑠 ) = ( Hom ‘ 𝑆 ) )
20	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = 𝐵 ) → 𝐻 = ( Hom ‘ 𝑆 ) )
21	19 20	eqtr4d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑠 ) = 𝐻 )
22		simplr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝑏 = 𝐵 )
23	22	mpteq1d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑥 ∈ 𝑏 ↦ ∪ ^◡ { 𝑥 } ) = ( 𝑥 ∈ 𝐵 ↦ ∪ ^◡ { 𝑥 } ) )
24		simpr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → ℎ = 𝐻 )
25	24	oveqd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑢 ℎ 𝑣 ) = ( 𝑢 𝐻 𝑣 ) )
26	25	mpteq1d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) = ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) )
27	22 22 26	mpoeq123dv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) )
28	23 27	opeq12d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ^◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) ⟩ = ⟨ ( 𝑥 ∈ 𝐵 ↦ ∪ ^◡ { 𝑥 } ) , ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) ⟩ )
29	17 21 28	csbied2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = 𝐵 ) → ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ^◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) ⟩ = ⟨ ( 𝑥 ∈ 𝐵 ↦ ∪ ^◡ { 𝑥 } ) , ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) ⟩ )
30	13 16 29	csbied2	⊢ ( ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) ∧ 𝑠 = 𝑆 ) → ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ^◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) ⟩ = ⟨ ( 𝑥 ∈ 𝐵 ↦ ∪ ^◡ { 𝑥 } ) , ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) ⟩ )
31	8 12 30	csbied2	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → ⦋ ( 𝑐 ×_c 𝑑 ) / 𝑠 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑠 ) / ℎ ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ∪ ^◡ { 𝑥 } ) , ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( 𝑓 ∈ ( 𝑢 ℎ 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) ⟩ = ⟨ ( 𝑥 ∈ 𝐵 ↦ ∪ ^◡ { 𝑥 } ) , ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) ⟩ )
32	1	elexd	⊢ ( 𝜑 → 𝐶 ∈ V )
33	2	elexd	⊢ ( 𝜑 → 𝐷 ∈ V )
34		opex	⊢ ⟨ ( 𝑥 ∈ 𝐵 ↦ ∪ ^◡ { 𝑥 } ) , ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) ⟩ ∈ V
35	34	a1i	⊢ ( 𝜑 → ⟨ ( 𝑥 ∈ 𝐵 ↦ ∪ ^◡ { 𝑥 } ) , ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) ⟩ ∈ V )
36	7 31 32 33 35	ovmpod	⊢ ( 𝜑 → ( 𝐶 swap_F 𝐷 ) = ⟨ ( 𝑥 ∈ 𝐵 ↦ ∪ ^◡ { 𝑥 } ) , ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ^◡ { 𝑓 } ) ) ⟩ )

Metamath Proof Explorer

Theorem swapfval

Proof