prcofvalg

Description: Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025)

	Ref	Expression
Hypotheses	prcofvalg.b	$⊢ B = D Func E$
	prcofvalg.n	$⊢ N = D Nat E$
	prcofvalg.f	$⊢ φ \to F \in U$
	prcofvalg.p	$⊢ φ \to P \in V$
	prcofvalg.d	$⊢ φ \to 1^{st} (P) = D$
	prcofvalg.e	$⊢ φ \to 2^{nd} (P) = E$
Assertion	prcofvalg	Could not format assertion : No typesetting found for \|- ( ph -> ( P -o.F F ) = <. ( k e. B \|-> ( k o.func F ) ) , ( k e. B , l e. B \|-> ( a e. ( k N l ) \|-> ( a o. ( 1st ` F ) ) ) ) >. ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		prcofvalg.b	$⊢ B = D Func E$
2		prcofvalg.n	$⊢ N = D Nat E$
3		prcofvalg.f	$⊢ φ \to F \in U$
4		prcofvalg.p	$⊢ φ \to P \in V$
5		prcofvalg.d	$⊢ φ \to 1^{st} (P) = D$
6		prcofvalg.e	$⊢ φ \to 2^{nd} (P) = E$
7		df-prcof	Could not format -o.F = ( p e. _V , f e. _V \|-> [_ ( 1st ` p ) / d ]_ [_ ( 2nd ` p ) / e ]_ [_ ( d Func e ) / b ]_ <. ( k e. b \|-> ( k o.func f ) ) , ( k e. b , l e. b \|-> ( a e. ( k ( d Nat e ) l ) \|-> ( a o. ( 1st ` f ) ) ) ) >. ) : No typesetting found for \|- -o.F = ( p e. _V , f e. _V \|-> [_ ( 1st ` p ) / d ]_ [_ ( 2nd ` p ) / e ]_ [_ ( d Func e ) / b ]_ <. ( k e. b \|-> ( k o.func f ) ) , ( k e. b , l e. b \|-> ( a e. ( k ( d Nat e ) l ) \|-> ( a o. ( 1st ` f ) ) ) ) >. ) with typecode \|-
8	7	a1i	Could not format ( ph -> -o.F = ( p e. _V , f e. _V \|-> [_ ( 1st ` p ) / d ]_ [_ ( 2nd ` p ) / e ]_ [_ ( d Func e ) / b ]_ <. ( k e. b \|-> ( k o.func f ) ) , ( k e. b , l e. b \|-> ( a e. ( k ( d Nat e ) l ) \|-> ( a o. ( 1st ` f ) ) ) ) >. ) ) : No typesetting found for \|- ( ph -> -o.F = ( p e. _V , f e. _V \|-> [_ ( 1st ` p ) / d ]_ [_ ( 2nd ` p ) / e ]_ [_ ( d Func e ) / b ]_ <. ( k e. b \|-> ( k o.func f ) ) , ( k e. b , l e. b \|-> ( a e. ( k ( d Nat e ) l ) \|-> ( a o. ( 1st ` f ) ) ) ) >. ) ) with typecode \|-
9		fvexd	$⊢ (φ \land (p = P \land f = F)) \to 1^{st} (p) \in V$
10		simprl	$⊢ (φ \land (p = P \land f = F)) \to p = P$
11	10	fveq2d	$⊢ (φ \land (p = P \land f = F)) \to 1^{st} (p) = 1^{st} (P)$
12	5	adantr	$⊢ (φ \land (p = P \land f = F)) \to 1^{st} (P) = D$
13	11 12	eqtrd	$⊢ (φ \land (p = P \land f = F)) \to 1^{st} (p) = D$
14		fvexd	$⊢ ((φ \land (p = P \land f = F)) \land d = D) \to 2^{nd} (p) \in V$
15	10	adantr	$⊢ ((φ \land (p = P \land f = F)) \land d = D) \to p = P$
16	15	fveq2d	$⊢ ((φ \land (p = P \land f = F)) \land d = D) \to 2^{nd} (p) = 2^{nd} (P)$
17	6	ad2antrr	$⊢ ((φ \land (p = P \land f = F)) \land d = D) \to 2^{nd} (P) = E$
18	16 17	eqtrd	$⊢ ((φ \land (p = P \land f = F)) \land d = D) \to 2^{nd} (p) = E$
19		ovexd	$⊢ (((φ \land (p = P \land f = F)) \land d = D) \land e = E) \to d Func e \in V$
20		simplr	$⊢ (((φ \land (p = P \land f = F)) \land d = D) \land e = E) \to d = D$
21		simpr	$⊢ (((φ \land (p = P \land f = F)) \land d = D) \land e = E) \to e = E$
22	20 21	oveq12d	$⊢ (((φ \land (p = P \land f = F)) \land d = D) \land e = E) \to d Func e = D Func E$
23	22 1	eqtr4di	$⊢ (((φ \land (p = P \land f = F)) \land d = D) \land e = E) \to d Func e = B$
24		simpr	$⊢ ((((φ \land (p = P \land f = F)) \land d = D) \land e = E) \land b = B) \to b = B$
25		simp-4r	$⊢ ((((φ \land (p = P \land f = F)) \land d = D) \land e = E) \land b = B) \to (p = P \land f = F)$
26	25	simprd	$⊢ ((((φ \land (p = P \land f = F)) \land d = D) \land e = E) \land b = B) \to f = F$
27	26	oveq2d	$⊢ ((((φ \land (p = P \land f = F)) \land d = D) \land e = E) \land b = B) \to k \circ_{func} f = k \circ_{func} F$
28	24 27	mpteq12dv	$⊢ ((((φ \land (p = P \land f = F)) \land d = D) \land e = E) \land b = B) \to (k \in b ⟼ k \circ_{func} f) = (k \in B ⟼ k \circ_{func} F)$
29	20 21	oveq12d	$⊢ (((φ \land (p = P \land f = F)) \land d = D) \land e = E) \to d Nat e = D Nat E$
30	29 2	eqtr4di	$⊢ (((φ \land (p = P \land f = F)) \land d = D) \land e = E) \to d Nat e = N$
31	30	oveqdr	$⊢ ((((φ \land (p = P \land f = F)) \land d = D) \land e = E) \land b = B) \to k (d Nat e) l = k N l$
32	26	fveq2d	$⊢ ((((φ \land (p = P \land f = F)) \land d = D) \land e = E) \land b = B) \to 1^{st} (f) = 1^{st} (F)$
33	32	coeq2d	$⊢ ((((φ \land (p = P \land f = F)) \land d = D) \land e = E) \land b = B) \to a \circ 1^{st} (f) = a \circ 1^{st} (F)$
34	31 33	mpteq12dv	$⊢ ((((φ \land (p = P \land f = F)) \land d = D) \land e = E) \land b = B) \to (a \in (k (d Nat e) l) ⟼ a \circ 1^{st} (f)) = (a \in (k N l) ⟼ a \circ 1^{st} (F))$
35	24 24 34	mpoeq123dv	$⊢ ((((φ \land (p = P \land f = F)) \land d = D) \land e = E) \land b = B) \to (k \in b, l \in b ⟼ (a \in (k (d Nat e) l) ⟼ a \circ 1^{st} (f))) = (k \in B, l \in B ⟼ (a \in (k N l) ⟼ a \circ 1^{st} (F)))$
36	28 35	opeq12d	$⊢ ((((φ \land (p = P \land f = F)) \land d = D) \land e = E) \land b = B) \to ⟨(k \in b ⟼ k \circ_{func} f), (k \in b, l \in b ⟼ (a \in (k (d Nat e) l) ⟼ a \circ 1^{st} (f)))⟩ = ⟨(k \in B ⟼ k \circ_{func} F), (k \in B, l \in B ⟼ (a \in (k N l) ⟼ a \circ 1^{st} (F)))⟩$
37	19 23 36	csbied2	$⊢ (((φ \land (p = P \land f = F)) \land d = D) \land e = E) \to ⦋ (d Func e) / b ⦌ ⟨(k \in b ⟼ k \circ_{func} f), (k \in b, l \in b ⟼ (a \in (k (d Nat e) l) ⟼ a \circ 1^{st} (f)))⟩ = ⟨(k \in B ⟼ k \circ_{func} F), (k \in B, l \in B ⟼ (a \in (k N l) ⟼ a \circ 1^{st} (F)))⟩$
38	14 18 37	csbied2	$⊢ ((φ \land (p = P \land f = F)) \land d = D) \to ⦋ 2^{nd} (p) / e ⦌ ⦋ (d Func e) / b ⦌ ⟨(k \in b ⟼ k \circ_{func} f), (k \in b, l \in b ⟼ (a \in (k (d Nat e) l) ⟼ a \circ 1^{st} (f)))⟩ = ⟨(k \in B ⟼ k \circ_{func} F), (k \in B, l \in B ⟼ (a \in (k N l) ⟼ a \circ 1^{st} (F)))⟩$
39	9 13 38	csbied2	$⊢ (φ \land (p = P \land f = F)) \to ⦋ 1^{st} (p) / d ⦌ ⦋ 2^{nd} (p) / e ⦌ ⦋ (d Func e) / b ⦌ ⟨(k \in b ⟼ k \circ_{func} f), (k \in b, l \in b ⟼ (a \in (k (d Nat e) l) ⟼ a \circ 1^{st} (f)))⟩ = ⟨(k \in B ⟼ k \circ_{func} F), (k \in B, l \in B ⟼ (a \in (k N l) ⟼ a \circ 1^{st} (F)))⟩$
40	4	elexd	$⊢ φ \to P \in V$
41	3	elexd	$⊢ φ \to F \in V$
42		opex	$⊢ ⟨(k \in B ⟼ k \circ_{func} F), (k \in B, l \in B ⟼ (a \in (k N l) ⟼ a \circ 1^{st} (F)))⟩ \in V$
43	42	a1i	$⊢ φ \to ⟨(k \in B ⟼ k \circ_{func} F), (k \in B, l \in B ⟼ (a \in (k N l) ⟼ a \circ 1^{st} (F)))⟩ \in V$
44	8 39 40 41 43	ovmpod	Could not format ( ph -> ( P -o.F F ) = <. ( k e. B \|-> ( k o.func F ) ) , ( k e. B , l e. B \|-> ( a e. ( k N l ) \|-> ( a o. ( 1st ` F ) ) ) ) >. ) : No typesetting found for \|- ( ph -> ( P -o.F F ) = <. ( k e. B \|-> ( k o.func F ) ) , ( k e. B , l e. B \|-> ( a e. ( k N l ) \|-> ( a o. ( 1st ` F ) ) ) ) >. ) with typecode \|-

Metamath Proof Explorer

Theorem prcofvalg

Proof