fucofvalne

Description: Value of the function giving the functor composition bifunctor, if C or D are not sets. (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Hypotheses	fucofvalne.c	⊢ ( 𝜑 → ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) )
	fucofvalne.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	fucofvalne.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⚬ )
	fucofvalne.w	⊢ ( 𝜑 → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
Assertion	fucofvalne	⊢ ( 𝜑 → ⚬ ≠ ⟨ ( ∘_func ↾ 𝑊 ) , ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		fucofvalne.c	⊢ ( 𝜑 → ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) )
2		fucofvalne.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
3		fucofvalne.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⚬ )
4		fucofvalne.w	⊢ ( 𝜑 → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
5		0ex	⊢ ∅ ∈ V
6	5	a1i	⊢ ( 𝜑 → ∅ ∈ V )
7		1st0	⊢ ( 1^st ‘ ∅ ) = ∅
8	7	a1i	⊢ ( 𝜑 → ( 1^st ‘ ∅ ) = ∅ )
9		2nd0	⊢ ( 2^nd ‘ ∅ ) = ∅
10	9	a1i	⊢ ( 𝜑 → ( 2^nd ‘ ∅ ) = ∅ )
11		opprc	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ⟨ 𝐶 , 𝐷 ⟩ = ∅ )
12	1 11	syl	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ = ∅ )
13	12	oveq1d	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ( ∅ ∘_F 𝐸 ) )
14	13 3	eqtr3d	⊢ ( 𝜑 → ( ∅ ∘_F 𝐸 ) = ⚬ )
15		eqidd	⊢ ( 𝜑 → ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) = ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) )
16	6 8 10 2 14 15	fucofvalg	⊢ ( 𝜑 → ⚬ = ⟨ ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) , ( 𝑢 ∈ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) , 𝑣 ∈ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( ∅ Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( ∅ Nat ∅ ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ ∅ ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )
17		opex	⊢ ⟨ ∅ , ∅ ⟩ ∈ V
18	17	snnz	⊢ { ⟨ ∅ , ∅ ⟩ } ≠ ∅
19	18	neii	⊢ ¬ { ⟨ ∅ , ∅ ⟩ } = ∅
20		ioran	⊢ ( ¬ ( { ⟨ ∅ , ∅ ⟩ } = ∅ ∨ { ⟨ ∅ , ∅ ⟩ } = ∅ ) ↔ ( ¬ { ⟨ ∅ , ∅ ⟩ } = ∅ ∧ ¬ { ⟨ ∅ , ∅ ⟩ } = ∅ ) )
21		xpeq0	⊢ ( ( { ⟨ ∅ , ∅ ⟩ } × { ⟨ ∅ , ∅ ⟩ } ) = ∅ ↔ ( { ⟨ ∅ , ∅ ⟩ } = ∅ ∨ { ⟨ ∅ , ∅ ⟩ } = ∅ ) )
22	21	biimpi	⊢ ( ( { ⟨ ∅ , ∅ ⟩ } × { ⟨ ∅ , ∅ ⟩ } ) = ∅ → ( { ⟨ ∅ , ∅ ⟩ } = ∅ ∨ { ⟨ ∅ , ∅ ⟩ } = ∅ ) )
23	22	con3i	⊢ ( ¬ ( { ⟨ ∅ , ∅ ⟩ } = ∅ ∨ { ⟨ ∅ , ∅ ⟩ } = ∅ ) → ¬ ( { ⟨ ∅ , ∅ ⟩ } × { ⟨ ∅ , ∅ ⟩ } ) = ∅ )
24	20 23	sylbir	⊢ ( ( ¬ { ⟨ ∅ , ∅ ⟩ } = ∅ ∧ ¬ { ⟨ ∅ , ∅ ⟩ } = ∅ ) → ¬ ( { ⟨ ∅ , ∅ ⟩ } × { ⟨ ∅ , ∅ ⟩ } ) = ∅ )
25	19 19 24	mp2an	⊢ ¬ ( { ⟨ ∅ , ∅ ⟩ } × { ⟨ ∅ , ∅ ⟩ } ) = ∅
26	2	0func	⊢ ( 𝜑 → ( ∅ Func 𝐸 ) = { ⟨ ∅ , ∅ ⟩ } )
27		0cat	⊢ ∅ ∈ Cat
28	27	a1i	⊢ ( 𝜑 → ∅ ∈ Cat )
29	28	0func	⊢ ( 𝜑 → ( ∅ Func ∅ ) = { ⟨ ∅ , ∅ ⟩ } )
30	26 29	xpeq12d	⊢ ( 𝜑 → ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) = ( { ⟨ ∅ , ∅ ⟩ } × { ⟨ ∅ , ∅ ⟩ } ) )
31		df-func	⊢ Func = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Base ‘ 𝑡 ) / 𝑏 ] ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑢 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝑢 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑡 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑢 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } )
32	31	reldmmpo	⊢ Rel dom Func
33		0nelrel0	⊢ ( Rel dom Func → ¬ ∅ ∈ dom Func )
34	32 33	ax-mp	⊢ ¬ ∅ ∈ dom Func
35	12	eleq1d	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∈ dom Func ↔ ∅ ∈ dom Func ) )
36	34 35	mtbiri	⊢ ( 𝜑 → ¬ ⟨ 𝐶 , 𝐷 ⟩ ∈ dom Func )
37		df-ov	⊢ ( 𝐶 Func 𝐷 ) = ( Func ‘ ⟨ 𝐶 , 𝐷 ⟩ )
38		ndmfv	⊢ ( ¬ ⟨ 𝐶 , 𝐷 ⟩ ∈ dom Func → ( Func ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = ∅ )
39	37 38	eqtrid	⊢ ( ¬ ⟨ 𝐶 , 𝐷 ⟩ ∈ dom Func → ( 𝐶 Func 𝐷 ) = ∅ )
40	39	xpeq2d	⊢ ( ¬ ⟨ 𝐶 , 𝐷 ⟩ ∈ dom Func → ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( ( 𝐷 Func 𝐸 ) × ∅ ) )
41		xp0	⊢ ( ( 𝐷 Func 𝐸 ) × ∅ ) = ∅
42	40 41	eqtrdi	⊢ ( ¬ ⟨ 𝐶 , 𝐷 ⟩ ∈ dom Func → ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ∅ )
43	36 42	syl	⊢ ( 𝜑 → ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ∅ )
44	30 43	eqeq12d	⊢ ( 𝜑 → ( ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ↔ ( { ⟨ ∅ , ∅ ⟩ } × { ⟨ ∅ , ∅ ⟩ } ) = ∅ ) )
45	25 44	mtbiri	⊢ ( 𝜑 → ¬ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
46		rescofuf	⊢ ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) : ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ⟶ ( ∅ Func 𝐸 )
47	46	fdmi	⊢ dom ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) = ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) )
48		rescofuf	⊢ ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) : ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ⟶ ( 𝐶 Func 𝐸 )
49	48	fdmi	⊢ dom ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) )
50	47 49	eqeq12i	⊢ ( dom ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) = dom ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ↔ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
51	50	biimpi	⊢ ( dom ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) = dom ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) → ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
52	51	con3i	⊢ ( ¬ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) → ¬ dom ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) = dom ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) )
53		dmeq	⊢ ( ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) = ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) → dom ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) = dom ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) )
54	53	con3i	⊢ ( ¬ dom ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) = dom ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) → ¬ ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) = ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) )
55	45 52 54	3syl	⊢ ( 𝜑 → ¬ ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) = ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) )
56	55	neqned	⊢ ( 𝜑 → ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) ≠ ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) )
57	4	reseq2d	⊢ ( 𝜑 → ( ∘_func ↾ 𝑊 ) = ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) )
58	56 57	neeqtrrd	⊢ ( 𝜑 → ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) ≠ ( ∘_func ↾ 𝑊 ) )
59		ovex	⊢ ( ∅ Func 𝐸 ) ∈ V
60		ovex	⊢ ( ∅ Func ∅ ) ∈ V
61	59 60	xpex	⊢ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ∈ V
62		fex	⊢ ( ( ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) : ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ⟶ ( ∅ Func 𝐸 ) ∧ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ∈ V ) → ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) ∈ V )
63	46 61 62	mp2an	⊢ ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) ∈ V
64	61 61	mpoex	⊢ ( 𝑢 ∈ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) , 𝑣 ∈ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( ∅ Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( ∅ Nat ∅ ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ ∅ ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ∈ V
65		opth1neg	⊢ ( ( ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) ∈ V ∧ ( 𝑢 ∈ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) , 𝑣 ∈ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( ∅ Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( ∅ Nat ∅ ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ ∅ ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ∈ V ) → ( ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) ≠ ( ∘_func ↾ 𝑊 ) → ⟨ ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) , ( 𝑢 ∈ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) , 𝑣 ∈ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( ∅ Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( ∅ Nat ∅ ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ ∅ ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ ≠ ⟨ ( ∘_func ↾ 𝑊 ) , ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ ) )
66	63 64 65	mp2an	⊢ ( ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) ≠ ( ∘_func ↾ 𝑊 ) → ⟨ ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) , ( 𝑢 ∈ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) , 𝑣 ∈ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( ∅ Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( ∅ Nat ∅ ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ ∅ ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ ≠ ⟨ ( ∘_func ↾ 𝑊 ) , ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )
67	58 66	syl	⊢ ( 𝜑 → ⟨ ( ∘_func ↾ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ) , ( 𝑢 ∈ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) , 𝑣 ∈ ( ( ∅ Func 𝐸 ) × ( ∅ Func ∅ ) ) ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( ∅ Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( ∅ Nat ∅ ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ ∅ ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ ≠ ⟨ ( ∘_func ↾ 𝑊 ) , ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )
68	16 67	eqnetrd	⊢ ( 𝜑 → ⚬ ≠ ⟨ ( ∘_func ↾ 𝑊 ) , ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )

Metamath Proof Explorer

Theorem fucofvalne

Proof