tposcurf1

Description: Value of the object part of the transposed curry functor. (Contributed by Zhi Wang, 9-Oct-2025)

	Ref	Expression
Hypotheses	tposcurf1.g	⊢ ( 𝜑 → 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) )
	tposcurf1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	tposcurf1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	tposcurf1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	tposcurf1.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐷 ×_c 𝐶 ) Func 𝐸 ) )
	tposcurf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	tposcurf1.k	⊢ ( 𝜑 → 𝐾 = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) )
	tposcurf1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	tposcurf1.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	tposcurf1.1	⊢ 1 = ( Id ‘ 𝐶 )
Assertion	tposcurf1	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑦 ( 1^st ‘ 𝐹 ) 𝑋 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑋 ⟩ ) ( 1 ‘ 𝑋 ) ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		tposcurf1.g	⊢ ( 𝜑 → 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) )
2		tposcurf1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		tposcurf1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		tposcurf1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5		tposcurf1.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐷 ×_c 𝐶 ) Func 𝐸 ) )
6		tposcurf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
7		tposcurf1.k	⊢ ( 𝜑 → 𝐾 = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) )
8		tposcurf1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
9		tposcurf1.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
10		tposcurf1.1	⊢ 1 = ( Id ‘ 𝐶 )
11	1	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) = ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) )
12	11	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) = ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 ) )
13		eqid	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) )
14		eqidd	⊢ ( 𝜑 → ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) = ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) )
15	3 4 5 14	cofuswapfcl	⊢ ( 𝜑 → ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
16		eqid	⊢ ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 ) = ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 )
17	13 2 3 4 15 8 6 16 9 10	curf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 ) = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ )
18	7 12 17	3eqtrd	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ )
19	8	fvexi	⊢ 𝐵 ∈ V
20	19	mptex	⊢ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) 𝑦 ) ) ∈ V
21	19 19	mpoex	⊢ ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ∈ V
22	20 21	op1std	⊢ ( 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ → ( 1^st ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) 𝑦 ) ) )
23	18 22	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) 𝑦 ) ) )
24		ovexd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑋 ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) 𝑦 ) ∈ V )
25	23 24	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) = ( 𝑋 ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) 𝑦 ) )
26	1	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) )
27	3	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ Cat )
28	4	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ Cat )
29	5	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐹 ∈ ( ( 𝐷 ×_c 𝐶 ) Func 𝐸 ) )
30	6	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑋 ∈ 𝐴 )
31	7	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐾 = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) )
32		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
33	26 2 27 28 29 30 31 8 32	tposcurf11	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) = ( 𝑦 ( 1^st ‘ 𝐹 ) 𝑋 ) )
34	25 33	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑋 ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) 𝑦 ) = ( 𝑦 ( 1^st ‘ 𝐹 ) 𝑋 ) )
35	34	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) 𝑦 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑦 ( 1^st ‘ 𝐹 ) 𝑋 ) ) )
36	20 21	op2ndd	⊢ ( 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ → ( 2^nd ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) )
37	18 36	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) )
38		ovex	⊢ ( 𝑦 𝐽 𝑧 ) ∈ V
39	38	mptex	⊢ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ∈ V
40	39	a1i	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ∈ V )
41	37 40	ovmpt4d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) = ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) )
42		ovexd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) → ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ∈ V )
43	41 42	fvmpt2d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) ‘ 𝑔 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) )
44	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) )
45	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝐶 ∈ Cat )
46	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝐷 ∈ Cat )
47	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝐹 ∈ ( ( 𝐷 ×_c 𝐶 ) Func 𝐸 ) )
48	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝑋 ∈ 𝐴 )
49	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝐾 = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) )
50		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝑦 ∈ 𝐵 )
51		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝑧 ∈ 𝐵 )
52		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) )
53	44 2 45 46 47 48 49 8 50 9 10 51 52	tposcurf12	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) ‘ 𝑔 ) = ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑋 ⟩ ) ( 1 ‘ 𝑋 ) ) )
54	43 53	eqtr3d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) → ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) = ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑋 ⟩ ) ( 1 ‘ 𝑋 ) ) )
55	54	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑋 ⟩ ) ( 1 ‘ 𝑋 ) ) ) )
56	55	3impb	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑋 ⟩ ) ( 1 ‘ 𝑋 ) ) ) )
57	56	mpoeq3dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑋 ⟩ ) ( 1 ‘ 𝑋 ) ) ) ) )
58	35 57	opeq12d	⊢ ( 𝜑 → ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑦 ( 1^st ‘ 𝐹 ) 𝑋 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑋 ⟩ ) ( 1 ‘ 𝑋 ) ) ) ) ⟩ )
59	18 58	eqtrd	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑦 ( 1^st ‘ 𝐹 ) 𝑋 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑋 ⟩ ) ( 1 ‘ 𝑋 ) ) ) ) ⟩ )

Metamath Proof Explorer

Theorem tposcurf1

Proof