upfval

Description: Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025)

	Ref	Expression
Hypotheses	upfval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	upfval.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
	upfval.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	upfval.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
	upfval.o	⊢ 𝑂 = ( comp ‘ 𝐸 )
Assertion	upfval	⊢ ( 𝐷 UP 𝐸 ) = ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑤 ∈ 𝐶 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		upfval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
2		upfval.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
3		upfval.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
4		upfval.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
5		upfval.o	⊢ 𝑂 = ( comp ‘ 𝐸 )
6		fvexd	⊢ ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) → ( Base ‘ 𝑑 ) ∈ V )
7		fveq2	⊢ ( 𝑑 = 𝐷 → ( Base ‘ 𝑑 ) = ( Base ‘ 𝐷 ) )
8	7	adantr	⊢ ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) → ( Base ‘ 𝑑 ) = ( Base ‘ 𝐷 ) )
9	8 1	eqtr4di	⊢ ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) → ( Base ‘ 𝑑 ) = 𝐵 )
10		fvexd	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( Base ‘ 𝑒 ) ∈ V )
11		simplr	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → 𝑒 = 𝐸 )
12	11	fveq2d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( Base ‘ 𝑒 ) = ( Base ‘ 𝐸 ) )
13	12 2	eqtr4di	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( Base ‘ 𝑒 ) = 𝐶 )
14		fvexd	⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) → ( Hom ‘ 𝑑 ) ∈ V )
15		simplll	⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) → 𝑑 = 𝐷 )
16	15	fveq2d	⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) → ( Hom ‘ 𝑑 ) = ( Hom ‘ 𝐷 ) )
17	16 3	eqtr4di	⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) → ( Hom ‘ 𝑑 ) = 𝐻 )
18		fvexd	⊢ ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) → ( Hom ‘ 𝑒 ) ∈ V )
19		simp-4r	⊢ ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) → 𝑒 = 𝐸 )
20	19	fveq2d	⊢ ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) → ( Hom ‘ 𝑒 ) = ( Hom ‘ 𝐸 ) )
21	20 4	eqtr4di	⊢ ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) → ( Hom ‘ 𝑒 ) = 𝐽 )
22		fvexd	⊢ ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) → ( comp ‘ 𝑒 ) ∈ V )
23		simp-5r	⊢ ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) → 𝑒 = 𝐸 )
24	23	fveq2d	⊢ ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) → ( comp ‘ 𝑒 ) = ( comp ‘ 𝐸 ) )
25	24 5	eqtr4di	⊢ ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) → ( comp ‘ 𝑒 ) = 𝑂 )
26		simp-6l	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → 𝑑 = 𝐷 )
27		simp-6r	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → 𝑒 = 𝐸 )
28	26 27	oveq12d	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( 𝑑 Func 𝑒 ) = ( 𝐷 Func 𝐸 ) )
29		simp-4r	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → 𝑐 = 𝐶 )
30		simp-5r	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → 𝑏 = 𝐵 )
31	30	eleq2d	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( 𝑥 ∈ 𝑏 ↔ 𝑥 ∈ 𝐵 ) )
32		simplr	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → 𝑗 = 𝐽 )
33	32	oveqd	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) = ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) )
34	33	eleq2d	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( 𝑚 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ↔ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) )
35	31 34	anbi12d	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( ( 𝑥 ∈ 𝑏 ∧ 𝑚 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) )
36	32	oveqd	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) = ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) )
37		simplr	⊢ ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) → ℎ = 𝐻 )
38	37	oveqdr	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( 𝑥 ℎ 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
39		simpr	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → 𝑜 = 𝑂 )
40	39	oveqd	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) )
41	40	oveqd	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) )
42	41	eqeq2d	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ↔ 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) )
43	38 42	reueqbidv	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( ∃! 𝑘 ∈ ( 𝑥 ℎ 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) )
44	36 43	raleqbidv	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( ∀ 𝑔 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ℎ 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) )
45	30 44	raleqbidv	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( ∀ 𝑦 ∈ 𝑏 ∀ 𝑔 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ℎ 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) )
46	35 45	anbi12d	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( ( ( 𝑥 ∈ 𝑏 ∧ 𝑚 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑔 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ℎ 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) ) )
47	46	opabbidv	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑚 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑔 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ℎ 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } = { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } )
48	28 29 47	mpoeq123dv	⊢ ( ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑜 = 𝑂 ) → ( 𝑓 ∈ ( 𝑑 Func 𝑒 ) , 𝑤 ∈ 𝑐 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑚 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑔 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ℎ 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) = ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑤 ∈ 𝐶 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) )
49	22 25 48	csbied2	⊢ ( ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) ∧ 𝑗 = 𝐽 ) → ⦋ ( comp ‘ 𝑒 ) / 𝑜 ⦌ ( 𝑓 ∈ ( 𝑑 Func 𝑒 ) , 𝑤 ∈ 𝑐 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑚 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑔 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ℎ 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) = ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑤 ∈ 𝐶 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) )
50	18 21 49	csbied2	⊢ ( ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ℎ = 𝐻 ) → ⦋ ( Hom ‘ 𝑒 ) / 𝑗 ⦌ ⦋ ( comp ‘ 𝑒 ) / 𝑜 ⦌ ( 𝑓 ∈ ( 𝑑 Func 𝑒 ) , 𝑤 ∈ 𝑐 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑚 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑔 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ℎ 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) = ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑤 ∈ 𝐶 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) )
51	14 17 50	csbied2	⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) → ⦋ ( Hom ‘ 𝑑 ) / ℎ ⦌ ⦋ ( Hom ‘ 𝑒 ) / 𝑗 ⦌ ⦋ ( comp ‘ 𝑒 ) / 𝑜 ⦌ ( 𝑓 ∈ ( 𝑑 Func 𝑒 ) , 𝑤 ∈ 𝑐 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑚 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑔 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ℎ 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) = ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑤 ∈ 𝐶 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) )
52	10 13 51	csbied2	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ⦋ ( Base ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( Hom ‘ 𝑑 ) / ℎ ⦌ ⦋ ( Hom ‘ 𝑒 ) / 𝑗 ⦌ ⦋ ( comp ‘ 𝑒 ) / 𝑜 ⦌ ( 𝑓 ∈ ( 𝑑 Func 𝑒 ) , 𝑤 ∈ 𝑐 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑚 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑔 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ℎ 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) = ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑤 ∈ 𝐶 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) )
53	6 9 52	csbied2	⊢ ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) → ⦋ ( Base ‘ 𝑑 ) / 𝑏 ⦌ ⦋ ( Base ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( Hom ‘ 𝑑 ) / ℎ ⦌ ⦋ ( Hom ‘ 𝑒 ) / 𝑗 ⦌ ⦋ ( comp ‘ 𝑒 ) / 𝑜 ⦌ ( 𝑓 ∈ ( 𝑑 Func 𝑒 ) , 𝑤 ∈ 𝑐 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑚 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑔 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ℎ 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) = ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑤 ∈ 𝐶 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) )
54		df-up	⊢ UP = ( 𝑑 ∈ V , 𝑒 ∈ V ↦ ⦋ ( Base ‘ 𝑑 ) / 𝑏 ⦌ ⦋ ( Base ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( Hom ‘ 𝑑 ) / ℎ ⦌ ⦋ ( Hom ‘ 𝑒 ) / 𝑗 ⦌ ⦋ ( comp ‘ 𝑒 ) / 𝑜 ⦌ ( 𝑓 ∈ ( 𝑑 Func 𝑒 ) , 𝑤 ∈ 𝑐 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑚 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑔 ∈ ( 𝑤 𝑗 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ℎ 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) )
55		ovex	⊢ ( 𝐷 Func 𝐸 ) ∈ V
56	2	fvexi	⊢ 𝐶 ∈ V
57	55 56	mpoex	⊢ ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑤 ∈ 𝐶 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) ∈ V
58	53 54 57	ovmpoa	⊢ ( ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) → ( 𝐷 UP 𝐸 ) = ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑤 ∈ 𝐶 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) )
59	54	reldmmpo	⊢ Rel dom UP
60	59	ovprc	⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) → ( 𝐷 UP 𝐸 ) = ∅ )
61		df-func	⊢ Func = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Base ‘ 𝑡 ) / 𝑏 ] ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑢 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝑢 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑡 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑢 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } )
62	61	reldmmpo	⊢ Rel dom Func
63	62	ovprc	⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) → ( 𝐷 Func 𝐸 ) = ∅ )
64	63	orcd	⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) → ( ( 𝐷 Func 𝐸 ) = ∅ ∨ 𝐶 = ∅ ) )
65		0mpo0	⊢ ( ( ( 𝐷 Func 𝐸 ) = ∅ ∨ 𝐶 = ∅ ) → ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑤 ∈ 𝐶 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) = ∅ )
66	64 65	syl	⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) → ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑤 ∈ 𝐶 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) = ∅ )
67	60 66	eqtr4d	⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) → ( 𝐷 UP 𝐸 ) = ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑤 ∈ 𝐶 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) )
68	58 67	pm2.61i	⊢ ( 𝐷 UP 𝐸 ) = ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑤 ∈ 𝐶 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } )

Metamath Proof Explorer

Theorem upfval

Proof